An exact proof term for the current goal is (well_ordered_set_is_ordinal X Hwo).

An exact proof term for the current goal is (ordinal_TransSet X HordX).

An exact proof term for the current goal is (order_topology_basis_cases X b HbB).

Assume H123: (((∃u ∈ X, ∃v ∈ X, b = {x ∈ X|order_rel X u x ∧ order_rel X x v}) ∨ (∃v ∈ X, b = {x ∈ X|order_rel X x v})) ∨ (∃u ∈ X, b = {x ∈ X|order_rel X u x})).

Apply H123 to the current goal.

Assume H12: ((∃u ∈ X, ∃v ∈ X, b = {x ∈ X|order_rel X u x ∧ order_rel X x v}) ∨ (∃v ∈ X, b = {x ∈ X|order_rel X x v})).

Apply H12 to the current goal.

Assume Hiv: (∃u ∈ X, ∃v ∈ X, b = {x ∈ X|order_rel X u x ∧ order_rel X x v}).

Apply Hiv to the current goal.

Let u be given.

Assume HuCore.

Apply HuCore to the current goal.

Assume HuX HvEx.

Apply HvEx to the current goal.

Let v be given.

Assume HvCore.

Apply HvCore to the current goal.

Assume HvX Hbdef.

We use u to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HuX.

We prove the intermediate claim Hbin: b = {x ∈ X|order_rel X u x ∧ order_rel X x v}.

An exact proof term for the current goal is Hbdef.

We prove the intermediate claim HaIn: a ∈ {x ∈ X|order_rel X u x ∧ order_rel X x v}.

rewrite the current goal using Hbin (from right to left).

An exact proof term for the current goal is Hab.

We prove the intermediate claim Haconj: order_rel X u a ∧ order_rel X a v.

An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X u x0 ∧ order_rel X x0 v) a HaIn).

We prove the intermediate claim Hua: order_rel X u a.

An exact proof term for the current goal is (andEL (order_rel X u a) (order_rel X a v) Haconj).

We prove the intermediate claim Hav: order_rel X a v.

An exact proof term for the current goal is (andER (order_rel X u a) (order_rel X a v) Haconj).

Apply andI to the current goal.

An exact proof term for the current goal is Hua.

Let z be given.

Assume HzI: z ∈ order_interval_right_closed X u a.

We will prove z ∈ b.

We prove the intermediate claim HzX: z ∈ X.

An exact proof term for the current goal is (SepE1 X (λz0 : set ⇒ order_rel X u z0 ∧ (z0 = a ∨ order_rel X z0 a)) z HzI).

We prove the intermediate claim Hzconj: order_rel X u z ∧ (z = a ∨ order_rel X z a).

An exact proof term for the current goal is (SepE2 X (λz0 : set ⇒ order_rel X u z0 ∧ (z0 = a ∨ order_rel X z0 a)) z HzI).

We prove the intermediate claim Huz: order_rel X u z.

An exact proof term for the current goal is (andEL (order_rel X u z) (z = a ∨ order_rel X z a) Hzconj).

We prove the intermediate claim HzleA: z = a ∨ order_rel X z a.

An exact proof term for the current goal is (andER (order_rel X u z) (z = a ∨ order_rel X z a) Hzconj).

rewrite the current goal using Hbdef (from left to right).

Apply (SepI X (λx0 : set ⇒ order_rel X u x0 ∧ order_rel X x0 v) z HzX) to the current goal.

Apply andI to the current goal.

An exact proof term for the current goal is Huz.

Apply HzleA to the current goal.

Assume Hza: z = a.

rewrite the current goal using Hza (from left to right).

An exact proof term for the current goal is Hav.

Assume Hza: order_rel X z a.

An exact proof term for the current goal is (order_rel_trans X z a v Hso HzX HaX HvX Hza Hav).

Assume Hlow: (∃v ∈ X, b = {x ∈ X|order_rel X x v}).

Apply Hlow to the current goal.

Let v be given.

Assume HvCore2.

Apply HvCore2 to the current goal.

Assume HvX Hbdef2.

We prove the intermediate claim HaIn: a ∈ {x ∈ X|order_rel X x v}.

rewrite the current goal using Hbdef2 (from right to left).

An exact proof term for the current goal is Hab.

We prove the intermediate claim Hav: order_rel X a v.

An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X x0 v) a HaIn).

We prove the intermediate claim Hexx: ∃x0 : set, x0 ∈ a.

An exact proof term for the current goal is (nonempty_has_element a Ha0).

Apply Hexx to the current goal.

Let x0 be given.

Assume Hx0a: x0 ∈ a.

We prove the intermediate claim Hx0X: x0 ∈ X.

We prove the intermediate claim HasubX: a ⊆ X.

An exact proof term for the current goal is (HtransX a HaX).

An exact proof term for the current goal is (HasubX x0 Hx0a).

We prove the intermediate claim Hx0aRel: order_rel X x0 a.

An exact proof term for the current goal is (mem_implies_order_rel_well_ordered X x0 a Hwo Hx0a).

We use x0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hx0X.

Apply andI to the current goal.

An exact proof term for the current goal is Hx0aRel.

Let z be given.

Assume HzI: z ∈ order_interval_right_closed X x0 a.

We will prove z ∈ b.

We prove the intermediate claim HzX: z ∈ X.

An exact proof term for the current goal is (SepE1 X (λz0 : set ⇒ order_rel X x0 z0 ∧ (z0 = a ∨ order_rel X z0 a)) z HzI).

We prove the intermediate claim Hzconj: order_rel X x0 z ∧ (z = a ∨ order_rel X z a).

An exact proof term for the current goal is (SepE2 X (λz0 : set ⇒ order_rel X x0 z0 ∧ (z0 = a ∨ order_rel X z0 a)) z HzI).

We prove the intermediate claim HzleA: z = a ∨ order_rel X z a.

An exact proof term for the current goal is (andER (order_rel X x0 z) (z = a ∨ order_rel X z a) Hzconj).

rewrite the current goal using Hbdef2 (from left to right).

Apply (SepI X (λt : set ⇒ order_rel X t v) z HzX) to the current goal.

Apply HzleA to the current goal.

Assume Hza: z = a.

rewrite the current goal using Hza (from left to right).

An exact proof term for the current goal is Hav.

Assume Hza: order_rel X z a.

An exact proof term for the current goal is (order_rel_trans X z a v Hso HzX HaX HvX Hza Hav).

Assume Hup: (∃u ∈ X, b = {x ∈ X|order_rel X u x}).

Apply Hup to the current goal.

Let u be given.

Assume HuCore2.

Apply HuCore2 to the current goal.

Assume HuX Hbdef3.

We prove the intermediate claim HaIn: a ∈ {x ∈ X|order_rel X u x}.

rewrite the current goal using Hbdef3 (from right to left).

An exact proof term for the current goal is Hab.

We prove the intermediate claim Hua: order_rel X u a.

An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X u x0) a HaIn).

We use u to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HuX.

Apply andI to the current goal.

An exact proof term for the current goal is Hua.

Let z be given.

Assume HzI: z ∈ order_interval_right_closed X u a.

We will prove z ∈ b.

We prove the intermediate claim HzX: z ∈ X.

An exact proof term for the current goal is (SepE1 X (λz0 : set ⇒ order_rel X u z0 ∧ (z0 = a ∨ order_rel X z0 a)) z HzI).

We prove the intermediate claim Hzconj: order_rel X u z ∧ (z = a ∨ order_rel X z a).

An exact proof term for the current goal is (SepE2 X (λz0 : set ⇒ order_rel X u z0 ∧ (z0 = a ∨ order_rel X z0 a)) z HzI).

We prove the intermediate claim Huz: order_rel X u z.

An exact proof term for the current goal is (andEL (order_rel X u z) (z = a ∨ order_rel X z a) Hzconj).

rewrite the current goal using Hbdef3 (from left to right).

An exact proof term for the current goal is (SepI X (λt : set ⇒ order_rel X u t) z HzX Huz).

Assume HbXeq: b = X.

We prove the intermediate claim Hexx: ∃x0 : set, x0 ∈ a.

An exact proof term for the current goal is (nonempty_has_element a Ha0).

Apply Hexx to the current goal.

Let x0 be given.

Assume Hx0a: x0 ∈ a.

We prove the intermediate claim Hx0X: x0 ∈ X.

We prove the intermediate claim HasubX: a ⊆ X.

An exact proof term for the current goal is (HtransX a HaX).

An exact proof term for the current goal is (HasubX x0 Hx0a).

We prove the intermediate claim Hx0aRel: order_rel X x0 a.

An exact proof term for the current goal is (mem_implies_order_rel_well_ordered X x0 a Hwo Hx0a).

We use x0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hx0X.

Apply andI to the current goal.

An exact proof term for the current goal is Hx0aRel.

Let z be given.

Assume HzI: z ∈ order_interval_right_closed X x0 a.

We will prove z ∈ b.

rewrite the current goal using HbXeq (from left to right).

An exact proof term for the current goal is (SepE1 X (λz0 : set ⇒ order_rel X x0 z0 ∧ (z0 = a ∨ order_rel X z0 a)) z HzI).