We will prove closure_of R R_lower_limit_topology ex17_17_interval_A = ex17_17_interval_A_closure_lower ∧ closure_of R R_C_topology ex17_17_interval_A = ex17_17_interval_A_closure_C ∧ closure_of R R_lower_limit_topology ex17_17_interval_B = ex17_17_interval_B_closure_lower ∧ closure_of R R_C_topology ex17_17_interval_B = ex17_17_interval_B_closure_lower.
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 x be given.
Assume Hx: x ∈ closure_of R R_lower_limit_topology ex17_17_interval_A.
An exact proof term for the current goal is (ex17_17_closure_A_lower_Subq x Hx).
Let x be given.
Assume Hx: x ∈ ex17_17_interval_A_closure_lower.
An exact proof term for the current goal is (ex17_17_closure_A_lower_Supq x Hx).
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ closure_of R R_C_topology ex17_17_interval_A.
An exact proof term for the current goal is (ex17_17_closure_A_C_Subq x Hx).
Let x be given.
Assume Hx: x ∈ ex17_17_interval_A_closure_C.
An exact proof term for the current goal is (ex17_17_closure_A_C_Supq x Hx).
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ closure_of R R_lower_limit_topology ex17_17_interval_B.
An exact proof term for the current goal is (ex17_17_closure_B_lower_Subq x Hx).
Let x be given.
Assume Hx: x ∈ ex17_17_interval_B_closure_lower.
An exact proof term for the current goal is (ex17_17_closure_B_lower_Supq x Hx).
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ closure_of R R_C_topology ex17_17_interval_B.
An exact proof term for the current goal is (ex17_17_closure_B_C_Subq x Hx).
Let x be given.
Assume Hx: x ∈ ex17_17_interval_B_closure_lower.
An exact proof term for the current goal is (ex17_17_closure_B_C_Supq x Hx).
∎