Let X and I be given.
Assume HI: I ∈ order_topology_basis X.
Set S1 to be the term {I0 ∈ đ’Ģ X|∃a ∈ X, ∃b ∈ X, I0 = {x ∈ X|order_rel X a x ∧ order_rel X x b}}.
Set S2 to be the term {I0 ∈ đ’Ģ X|∃b ∈ X, I0 = {x ∈ X|order_rel X x b}}.
Set S3 to be the term {I0 ∈ đ’Ģ X|∃a ∈ X, I0 = {x ∈ X|order_rel X a x}}.
Set S12 to be the term S1 âˆĒ S2.
Set S123 to be the term S12 âˆĒ S3.
Set SX to be the term {X}.
We prove the intermediate claim Hdef: order_topology_basis X = (S123 âˆĒ SX).
Use reflexivity.
We prove the intermediate claim HI': I ∈ (S123 âˆĒ SX).
rewrite the current goal using Hdef (from right to left).
An exact proof term for the current goal is HI.
Apply (binunionE' S123 SX I (((((∃a ∈ X, ∃b ∈ X, I = {x ∈ X|order_rel X a x ∧ order_rel X x b}) ∨ (∃b ∈ X, I = {x ∈ X|order_rel X x b})) ∨ (∃a ∈ X, I = {x ∈ X|order_rel X a x})) ∨ I = X))) to the current goal.
Assume HIS123: I ∈ S123.
Apply (binunionE' S12 S3 I (((((∃a ∈ X, ∃b ∈ X, I = {x ∈ X|order_rel X a x ∧ order_rel X x b}) ∨ (∃b ∈ X, I = {x ∈ X|order_rel X x b})) ∨ (∃a ∈ X, I = {x ∈ X|order_rel X a x})) ∨ I = X))) to the current goal.
Assume HIS12: I ∈ S12.
Apply (binunionE' S1 S2 I (((((∃a ∈ X, ∃b ∈ X, I = {x ∈ X|order_rel X a x ∧ order_rel X x b}) ∨ (∃b ∈ X, I = {x ∈ X|order_rel X x b})) ∨ (∃a ∈ X, I = {x ∈ X|order_rel X a x})) ∨ I = X))) to the current goal.
Assume HIS1: I ∈ S1.
Apply orIL to the current goal.
Apply orIL to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is (SepE2 (đ’Ģ X) (ÎģI0 : set ⇒ ∃a ∈ X, ∃b ∈ X, I0 = {x ∈ X|order_rel X a x ∧ order_rel X x b}) I HIS1).
Assume HIS2: I ∈ S2.
Apply orIL to the current goal.
Apply orIL to the current goal.
Apply orIR to the current goal.
An exact proof term for the current goal is (SepE2 (đ’Ģ X) (ÎģI0 : set ⇒ ∃b ∈ X, I0 = {x ∈ X|order_rel X x b}) I HIS2).
An exact proof term for the current goal is HIS12.
Assume HIS3: I ∈ S3.
Apply orIL to the current goal.
Apply orIR to the current goal.
An exact proof term for the current goal is (SepE2 (đ’Ģ X) (ÎģI0 : set ⇒ ∃a ∈ X, I0 = {x ∈ X|order_rel X a x}) I HIS3).
An exact proof term for the current goal is HIS123.
Assume HISX: I ∈ SX.
Apply orIR to the current goal.
An exact proof term for the current goal is (SingE X I HISX).
An exact proof term for the current goal is HI'.
∎