We will prove closure_of ordered_square ordered_square_topology ordsq_A = ordsq_A ∪ {ordsq_p01} ∧ closure_of ordered_square ordered_square_topology ordsq_B = ordsq_B ∪ {ordsq_p10} ∧ closure_of ordered_square ordered_square_topology ordsq_C = ordsq_C_closure ∧ closure_of ordered_square ordered_square_topology ordsq_D = ordsq_D_closure ∧ closure_of ordered_square ordered_square_topology ordsq_E = ordsq_E_closure.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply set_ext to the current goal.
Let p be given.
Assume Hpcl: p ∈ closure_of ordered_square ordered_square_topology ordsq_A.
We will prove p ∈ ordsq_A ∪ {ordsq_p01}.
An exact proof term for the current goal is (ex17_18_closure_A_Subq p Hpcl).
Let p be given.
Assume HpU: p ∈ ordsq_A ∪ {ordsq_p01}.
We will prove p ∈ closure_of ordered_square ordered_square_topology ordsq_A.
An exact proof term for the current goal is (ex17_18_closure_A_Supq p HpU).
An exact proof term for the current goal is ex17_18_closure_B_eq.
An exact proof term for the current goal is ex17_18_closure_C_eq.
An exact proof term for the current goal is ex17_18_closure_D_eq.
An exact proof term for the current goal is ex17_18_closure_E.
∎