Let X be given.
Assume Hwo: well_ordered_set X.
Assume Hso: simply_ordered_set X.
We will prove normal_space X (order_topology X).
We will prove one_point_sets_closed X (order_topology X) ∧ ∀A B : set, closed_in X (order_topology X) A → closed_in X (order_topology X) B → A ∩ B = Empty → ∃U V : set, U ∈ order_topology X ∧ V ∈ order_topology X ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty.
Apply andI to the current goal.
We prove the intermediate claim HH: Hausdorff_space X (order_topology X).
An exact proof term for the current goal is (ex17_10_order_topology_Hausdorff X Hso).
An exact proof term for the current goal is (Hausdorff_one_point_sets_closed X (order_topology X) HH).
Let A and B be given.
Assume HAcl: closed_in X (order_topology X) A.
Assume HBcl: closed_in X (order_topology X) B.
Assume HABdisj: A ∩ B = Empty.
We will prove ∃U V : set, U ∈ order_topology X ∧ V ∈ order_topology X ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty.
We prove the intermediate claim HTx: topology_on X (order_topology X).
An exact proof term for the current goal is (order_topology_is_topology X Hso).
We prove the intermediate claim HAsubX: A ⊆ X.
An exact proof term for the current goal is (closed_in_subset X (order_topology X) A HAcl).
We prove the intermediate claim HBsubX: B ⊆ X.
An exact proof term for the current goal is (closed_in_subset X (order_topology X) B HBcl).
Apply (xm (A = Empty)) to the current goal.
Assume HAe: A = Empty.
We use Empty to witness the existential quantifier.
We use X to witness the existential quantifier.
Apply and5I to the current goal.
An exact proof term for the current goal is (topology_has_empty X (order_topology X) HTx).
An exact proof term for the current goal is (topology_has_X X (order_topology X) HTx).
rewrite the current goal using HAe (from left to right).
An exact proof term for the current goal is (Subq_Empty Empty).
An exact proof term for the current goal is HBsubX.
An exact proof term for the current goal is (binintersect_Empty_left X).
Assume HAnE: ¬ (A = Empty).
Apply (xm (B = Empty)) to the current goal.
Assume HBe: B = Empty.
We use X to witness the existential quantifier.
We use Empty to witness the existential quantifier.
Apply and5I to the current goal.
An exact proof term for the current goal is (topology_has_X X (order_topology X) HTx).
An exact proof term for the current goal is (topology_has_empty X (order_topology X) HTx).
An exact proof term for the current goal is HAsubX.
rewrite the current goal using HBe (from left to right).
An exact proof term for the current goal is (Subq_Empty Empty).
An exact proof term for the current goal is (binintersect_Empty_right X).
Assume HBnE: ¬ (B = Empty).
We prove the intermediate claim HexUB: ∃UB ∈ order_topology X, B = X ∖ UB.
An exact proof term for the current goal is (closed_in_exists_open_complement X (order_topology X) B HBcl).
Set UB to be the term Eps_i (λU : set ⇒ U ∈ order_topology X ∧ B = X ∖ U).
We prove the intermediate claim HUB: UB ∈ order_topology X ∧ B = X ∖ UB.
An exact proof term for the current goal is (Eps_i_ex (λU : set ⇒ U ∈ order_topology X ∧ B = X ∖ U) HexUB).
We prove the intermediate claim HUBTx: UB ∈ order_topology X.
An exact proof term for the current goal is (andEL (UB ∈ order_topology X) (B = X ∖ UB) HUB).
We prove the intermediate claim HBdef: B = X ∖ UB.
An exact proof term for the current goal is (andER (UB ∈ order_topology X) (B = X ∖ UB) HUB).
We prove the intermediate claim HexVA: ∃VA ∈ order_topology X, A = X ∖ VA.
An exact proof term for the current goal is (closed_in_exists_open_complement X (order_topology X) A HAcl).
Set VA to be the term Eps_i (λU : set ⇒ U ∈ order_topology X ∧ A = X ∖ U).
We prove the intermediate claim HVA: VA ∈ order_topology X ∧ A = X ∖ VA.
An exact proof term for the current goal is (Eps_i_ex (λU : set ⇒ U ∈ order_topology X ∧ A = X ∖ U) HexVA).
We prove the intermediate claim HVATx: VA ∈ order_topology X.
An exact proof term for the current goal is (andEL (VA ∈ order_topology X) (A = X ∖ VA) HVA).
We prove the intermediate claim HAdef: A = X ∖ VA.
An exact proof term for the current goal is (andER (VA ∈ order_topology X) (A = X ∖ VA) HVA).
Apply (xm (0 ∈ A)) to the current goal.
Assume H0A: 0 ∈ A.
An exact proof term for the current goal is (well_ordered_sets_normal_case_0_in_A X A B Hwo Hso HAcl HBcl HABdisj HAnE HBnE H0A).
Assume H0An: ¬ (0 ∈ A).
Apply (xm (0 ∈ B)) to the current goal.
Assume H0B: 0 ∈ B.
An exact proof term for the current goal is (well_ordered_sets_normal_case_0_in_B X A B Hwo Hso HAcl HBcl HABdisj HAnE HBnE H0B).
Assume H0Bn: ¬ (0 ∈ B).
We prove the intermediate claim HAsubUB: A ⊆ UB.
Let a be given.
Assume HaA: a ∈ A.
We will prove a ∈ UB.
We prove the intermediate claim HaX: a ∈ X.
An exact proof term for the current goal is (HAsubX a HaA).
Apply (xm (a ∈ UB)) to the current goal.
Assume HaUB: a ∈ UB.
An exact proof term for the current goal is HaUB.
Assume HaNotUB: ¬ (a ∈ UB).
We prove the intermediate claim HaXB: a ∈ X ∖ UB.
An exact proof term for the current goal is (setminusI X UB a HaX HaNotUB).
We prove the intermediate claim HaB: a ∈ B.
rewrite the current goal using HBdef (from left to right).
An exact proof term for the current goal is HaXB.
We prove the intermediate claim HaAB: a ∈ A ∩ B.
An exact proof term for the current goal is (binintersectI A B a HaA HaB).
We prove the intermediate claim HaE: a ∈ Empty.
An exact proof term for the current goal is (HABdisj (λU V : set ⇒ a ∈ U) HaAB).
An exact proof term for the current goal is (EmptyE a HaE (a ∈ UB)).
We prove the intermediate claim HBsubVA: B ⊆ VA.
Let b be given.
Assume HbB: b ∈ B.
We will prove b ∈ VA.
We prove the intermediate claim HbX: b ∈ X.
An exact proof term for the current goal is (HBsubX b HbB).
Apply (xm (b ∈ VA)) to the current goal.
Assume HbVA: b ∈ VA.
An exact proof term for the current goal is HbVA.
Assume HbNotVA: ¬ (b ∈ VA).
We prove the intermediate claim HbXA: b ∈ X ∖ VA.
An exact proof term for the current goal is (setminusI X VA b HbX HbNotVA).
We prove the intermediate claim HbA: b ∈ A.
rewrite the current goal using HAdef (from left to right).
An exact proof term for the current goal is HbXA.
We prove the intermediate claim HbAB: b ∈ A ∩ B.
An exact proof term for the current goal is (binintersectI A B b HbA HbB).
We prove the intermediate claim HbE: b ∈ Empty.
An exact proof term for the current goal is (HABdisj (λU V : set ⇒ b ∈ U) HbAB).
An exact proof term for the current goal is (EmptyE b HbE (b ∈ VA)).
We prove the intermediate claim HexA_basis: ∀a : set, a ∈ A → ∃b ∈ order_topology_basis X, a ∈ b ∧ b ⊆ UB.
Let a be given.
Assume HaA: a ∈ A.
We prove the intermediate claim HaUB: a ∈ UB.
An exact proof term for the current goal is (HAsubUB a HaA).
An exact proof term for the current goal is (order_topology_local_basis_elem X UB a Hso HUBTx HaUB).
An exact proof term for the current goal is (well_ordered_sets_normal_case_nonzero X A B UB VA Hwo Hso HTx HAcl HBcl HABdisj HAnE HBnE HUBTx HBdef HVATx HAdef H0An H0Bn).
∎