Let a and b be given.
Assume HaR HbR.
Set A to be the term {I ∈ đ’Ģ R|∃a1 ∈ R, ∃b1 ∈ R, I = {x ∈ R|order_rel R a1 x ∧ order_rel R x b1}}.
Set B to be the term {I ∈ đ’Ģ R|∃b1 ∈ R, I = {x ∈ R|order_rel R x b1}}.
Set C to be the term {I ∈ đ’Ģ R|∃a1 ∈ R, I = {x ∈ R|order_rel R a1 x}}.
We prove the intermediate claim HPow: open_interval a b ∈ đ’Ģ R.
An exact proof term for the current goal is (PowerI R (open_interval a b) (open_interval_Subq_R a b)).
We prove the intermediate claim HintEq: {x ∈ R|order_rel R a x ∧ order_rel R x b} = open_interval a b.
Apply set_ext to the current goal.
Let x be given.
Assume HxI: x ∈ {x0 ∈ R|order_rel R a x0 ∧ order_rel R x0 b}.
We will prove x ∈ open_interval a b.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (SepE1 R (Îģx0 : set ⇒ order_rel R a x0 ∧ order_rel R x0 b) x HxI).
We prove the intermediate claim Hconj: order_rel R a x ∧ order_rel R x b.
An exact proof term for the current goal is (SepE2 R (Îģx0 : set ⇒ order_rel R a x0 ∧ order_rel R x0 b) x HxI).
We prove the intermediate claim Hax: order_rel R a x.
An exact proof term for the current goal is (andEL (order_rel R a x) (order_rel R x b) Hconj).
We prove the intermediate claim Hxb: order_rel R x b.
An exact proof term for the current goal is (andER (order_rel R a x) (order_rel R x b) Hconj).
We prove the intermediate claim Haxlt: Rlt a x.
An exact proof term for the current goal is (order_rel_R_implies_Rlt a x Hax).
We prove the intermediate claim Hxblt: Rlt x b.
An exact proof term for the current goal is (order_rel_R_implies_Rlt x b Hxb).
An exact proof term for the current goal is (SepI R (Îģx0 : set ⇒ Rlt a x0 ∧ Rlt x0 b) x HxR (andI (Rlt a x) (Rlt x b) Haxlt Hxblt)).
Let x be given.
Assume HxI: x ∈ open_interval a b.
We will prove x ∈ {x0 ∈ R|order_rel R a x0 ∧ order_rel R x0 b}.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (SepE1 R (Îģx0 : set ⇒ Rlt a x0 ∧ Rlt x0 b) x HxI).
We prove the intermediate claim Hconj: Rlt a x ∧ Rlt x b.
An exact proof term for the current goal is (SepE2 R (Îģx0 : set ⇒ Rlt a x0 ∧ Rlt x0 b) x HxI).
We prove the intermediate claim Hax: Rlt a x.
An exact proof term for the current goal is (andEL (Rlt a x) (Rlt x b) Hconj).
We prove the intermediate claim Hxb: Rlt x b.
An exact proof term for the current goal is (andER (Rlt a x) (Rlt x b) Hconj).
We prove the intermediate claim Haxrel: order_rel R a x.
An exact proof term for the current goal is (Rlt_implies_order_rel_R a x Hax).
We prove the intermediate claim Hxbrel: order_rel R x b.
An exact proof term for the current goal is (Rlt_implies_order_rel_R x b Hxb).
An exact proof term for the current goal is (SepI R (Îģx0 : set ⇒ order_rel R a x0 ∧ order_rel R x0 b) x HxR (andI (order_rel R a x) (order_rel R x b) Haxrel Hxbrel)).
We prove the intermediate claim Hpred: ∃a0 ∈ R, ∃b0 ∈ R, open_interval a b = {x ∈ R|order_rel R a0 x ∧ order_rel R x b0}.
We use a to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HaR.
We use b to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HbR.
rewrite the current goal using HintEq (from left to right).
Use reflexivity.
We prove the intermediate claim HInA: open_interval a b ∈ A.
An exact proof term for the current goal is (SepI (đ’Ģ R) (ÎģI0 : set ⇒ ∃a0 ∈ R, ∃b0 ∈ R, I0 = {x ∈ R|order_rel R a0 x ∧ order_rel R x b0}) (open_interval a b) HPow Hpred).
We prove the intermediate claim HInAB: open_interval a b ∈ (A âˆĒ B).
An exact proof term for the current goal is (binunionI1 A B (open_interval a b) HInA).
Set Bold to be the term (A âˆĒ B âˆĒ C).
An exact proof term for the current goal is (binunionI1 Bold {R} (open_interval a b) (binunionI1 (A âˆĒ B) C (open_interval a b) HInAB)).
∎