We will prove K ≠ Empty ∧ partial_order_on K (rel_restrict le K).

Apply andI to the current goal.

Assume HK0: K = Empty.

We will prove False.

We prove the intermediate claim HJne: J ≠ Empty.

An exact proof term for the current goal is (directed_set_nonempty J le HJ).

We prove the intermediate claim Hexj: ∃j0 : set, j0 ∈ J.

An exact proof term for the current goal is (nonempty_has_element J HJne).

Apply Hexj to the current goal.

Let j0 be given.

Assume Hj0: j0 ∈ J.

We prove the intermediate claim Hexk: ∃k0 : set, k0 ∈ K ∧ (j0,k0) ∈ le.

An exact proof term for the current goal is (Hcofinal j0 Hj0).

Apply Hexk to the current goal.

Let k0 be given.

Assume Hk0pair.

We prove the intermediate claim Hk0K: k0 ∈ K.

An exact proof term for the current goal is (andEL (k0 ∈ K) ((j0,k0) ∈ le) Hk0pair).

We prove the intermediate claim Hk0E: k0 ∈ Empty.

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

An exact proof term for the current goal is Hk0K.

An exact proof term for the current goal is (EmptyE k0 Hk0E).

We will prove partial_order_on K (rel_restrict le K).

Apply HJ to the current goal.

Assume Hleft Hdir.

Apply Hleft to the current goal.

Assume HJne Hpo.

We will prove relation_on (rel_restrict le K) K ∧ (∀a : set, a ∈ K → (a,a) ∈ rel_restrict le K) ∧ (∀a b : set, a ∈ K → b ∈ K → (a,b) ∈ rel_restrict le K → (b,a) ∈ rel_restrict le K → a = b) ∧ (∀a b c : set, a ∈ K → b ∈ K → c ∈ K → (a,b) ∈ rel_restrict le K → (b,c) ∈ rel_restrict le K → (a,c) ∈ rel_restrict le K).

We prove the intermediate claim Hrefl: ∀a : set, a ∈ J → (a,a) ∈ le.

An exact proof term for the current goal is (partial_order_on_refl J le Hpo).

We prove the intermediate claim Hantisym: ∀a b : set, a ∈ J → b ∈ J → (a,b) ∈ le → (b,a) ∈ le → a = b.

An exact proof term for the current goal is (partial_order_on_antisym J le Hpo).

We prove the intermediate claim Htrans: ∀a b c : set, a ∈ J → b ∈ J → c ∈ J → (a,b) ∈ le → (b,c) ∈ le → (a,c) ∈ le.

An exact proof term for the current goal is (partial_order_on_trans J le Hpo).

Apply andI to the current goal.

We will prove relation_on (rel_restrict le K) K.

We will prove ∀a b : set, (a,b) ∈ rel_restrict le K → a ∈ K ∧ b ∈ K.

Let a and b be given.

Assume Hab: (a,b) ∈ rel_restrict le K.

We will prove a ∈ K ∧ b ∈ K.

We prove the intermediate claim Hab3: (a,b) ∈ le ∧ a ∈ K ∧ b ∈ K.

An exact proof term for the current goal is (rel_restrictE le K a b Hab).

We prove the intermediate claim Hab2: (a,b) ∈ le ∧ a ∈ K.

An exact proof term for the current goal is (andEL ((a,b) ∈ le ∧ a ∈ K) (b ∈ K) Hab3).

We prove the intermediate claim HaK: a ∈ K.

An exact proof term for the current goal is (andER ((a,b) ∈ le) (a ∈ K) Hab2).

We prove the intermediate claim HbK: b ∈ K.

An exact proof term for the current goal is (andER ((a,b) ∈ le ∧ a ∈ K) (b ∈ K) Hab3).

Apply andI to the current goal.

We will prove a ∈ K.

An exact proof term for the current goal is HaK.

We will prove b ∈ K.

An exact proof term for the current goal is HbK.

Let a be given.

Assume HaK: a ∈ K.

We will prove (a,a) ∈ rel_restrict le K.

We prove the intermediate claim HaJ: a ∈ J.

An exact proof term for the current goal is (HK a HaK).

We prove the intermediate claim Haa: (a,a) ∈ le.

An exact proof term for the current goal is (Hrefl a HaJ).

An exact proof term for the current goal is (rel_restrictI le K a a Haa HaK HaK).

Let a and b be given.

Assume HaK: a ∈ K.

Assume HbK: b ∈ K.

Assume HabK: (a,b) ∈ rel_restrict le K.

Assume HbaK: (b,a) ∈ rel_restrict le K.

We will prove a = b.

We prove the intermediate claim HaJ: a ∈ J.

An exact proof term for the current goal is (HK a HaK).

We prove the intermediate claim HbJ: b ∈ J.

An exact proof term for the current goal is (HK b HbK).

We prove the intermediate claim Hab: (a,b) ∈ le.

We prove the intermediate claim Hab3: (a,b) ∈ le ∧ a ∈ K ∧ b ∈ K.

An exact proof term for the current goal is (rel_restrictE le K a b HabK).

We prove the intermediate claim Hab2: (a,b) ∈ le ∧ a ∈ K.

An exact proof term for the current goal is (andEL ((a,b) ∈ le ∧ a ∈ K) (b ∈ K) Hab3).

An exact proof term for the current goal is (andEL ((a,b) ∈ le) (a ∈ K) Hab2).

We prove the intermediate claim Hba: (b,a) ∈ le.

We prove the intermediate claim Hba3: (b,a) ∈ le ∧ b ∈ K ∧ a ∈ K.

An exact proof term for the current goal is (rel_restrictE le K b a HbaK).

We prove the intermediate claim Hba2: (b,a) ∈ le ∧ b ∈ K.

An exact proof term for the current goal is (andEL ((b,a) ∈ le ∧ b ∈ K) (a ∈ K) Hba3).

An exact proof term for the current goal is (andEL ((b,a) ∈ le) (b ∈ K) Hba2).

An exact proof term for the current goal is (Hantisym a b HaJ HbJ Hab Hba).

Let a, b and c be given.

Assume HaK: a ∈ K.

Assume HbK: b ∈ K.

Assume HcK: c ∈ K.

Assume HabK: (a,b) ∈ rel_restrict le K.

Assume HbcK: (b,c) ∈ rel_restrict le K.

We will prove (a,c) ∈ rel_restrict le K.

We prove the intermediate claim HaJ: a ∈ J.

An exact proof term for the current goal is (HK a HaK).

We prove the intermediate claim HbJ: b ∈ J.

An exact proof term for the current goal is (HK b HbK).

We prove the intermediate claim HcJ: c ∈ J.

An exact proof term for the current goal is (HK c HcK).

We prove the intermediate claim Hab: (a,b) ∈ le.

We prove the intermediate claim Hab3: (a,b) ∈ le ∧ a ∈ K ∧ b ∈ K.

An exact proof term for the current goal is (rel_restrictE le K a b HabK).

We prove the intermediate claim Hab2: (a,b) ∈ le ∧ a ∈ K.

An exact proof term for the current goal is (andEL ((a,b) ∈ le ∧ a ∈ K) (b ∈ K) Hab3).

An exact proof term for the current goal is (andEL ((a,b) ∈ le) (a ∈ K) Hab2).

We prove the intermediate claim Hbc: (b,c) ∈ le.

We prove the intermediate claim Hbc3: (b,c) ∈ le ∧ b ∈ K ∧ c ∈ K.

An exact proof term for the current goal is (rel_restrictE le K b c HbcK).

We prove the intermediate claim Hbc2: (b,c) ∈ le ∧ b ∈ K.

An exact proof term for the current goal is (andEL ((b,c) ∈ le ∧ b ∈ K) (c ∈ K) Hbc3).

An exact proof term for the current goal is (andEL ((b,c) ∈ le) (b ∈ K) Hbc2).

We prove the intermediate claim Hac: (a,c) ∈ le.

An exact proof term for the current goal is (Htrans a b c HaJ HbJ HcJ Hab Hbc).

An exact proof term for the current goal is (rel_restrictI le K a c Hac HaK HcK).

Let a and b be given.

Assume HaK: a ∈ K.

Assume HbK: b ∈ K.

We will prove ∃c : set, c ∈ K ∧ (a,c) ∈ rel_restrict le K ∧ (b,c) ∈ rel_restrict le K.

Apply HJ to the current goal.

Assume Hleft Hdir.

Apply Hleft to the current goal.

Assume HJne Hpo.

We prove the intermediate claim Htrans: ∀a b c : set, a ∈ J → b ∈ J → c ∈ J → (a,b) ∈ le → (b,c) ∈ le → (a,c) ∈ le.

An exact proof term for the current goal is (partial_order_on_trans J le Hpo).

We prove the intermediate claim HaJ: a ∈ J.

An exact proof term for the current goal is (HK a HaK).

We prove the intermediate claim HbJ: b ∈ J.

An exact proof term for the current goal is (HK b HbK).

We prove the intermediate claim Hexm: ∃m : set, m ∈ J ∧ (a,m) ∈ le ∧ (b,m) ∈ le.

An exact proof term for the current goal is (Hdir a b HaJ HbJ).

Apply Hexm to the current goal.

Let m be given.

Assume Hm.

Apply Hm to the current goal.

Assume Hmleft Hbm.

Apply Hmleft to the current goal.

Assume HmJ Ham.

We prove the intermediate claim Hexk: ∃k : set, k ∈ K ∧ (m,k) ∈ le.

An exact proof term for the current goal is (Hcofinal m HmJ).

Apply Hexk to the current goal.

Let k be given.

Assume Hkpair.

We prove the intermediate claim HkK: k ∈ K.

An exact proof term for the current goal is (andEL (k ∈ K) ((m,k) ∈ le) Hkpair).

We prove the intermediate claim Hmk: (m,k) ∈ le.

An exact proof term for the current goal is (andER (k ∈ K) ((m,k) ∈ le) Hkpair).

We prove the intermediate claim HkJ: k ∈ J.

An exact proof term for the current goal is (HK k HkK).

We prove the intermediate claim Hak: (a,k) ∈ le.

An exact proof term for the current goal is (Htrans a m k HaJ HmJ HkJ Ham Hmk).

We prove the intermediate claim Hbk: (b,k) ∈ le.

An exact proof term for the current goal is (Htrans b m k HbJ HmJ HkJ Hbm Hmk).

We use k to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HkK.

We will prove (a,k) ∈ {p ∈ le|p 0 ∈ K ∧ p 1 ∈ K}.

Apply (SepI le (λp : set ⇒ p 0 ∈ K ∧ p 1 ∈ K) (a,k) Hak) to the current goal.

Apply andI to the current goal.

rewrite the current goal using (tuple_2_0_eq a k) (from left to right).

An exact proof term for the current goal is HaK.

rewrite the current goal using (tuple_2_1_eq a k) (from left to right).

An exact proof term for the current goal is HkK.

We will prove (b,k) ∈ {p ∈ le|p 0 ∈ K ∧ p 1 ∈ K}.

Apply (SepI le (λp : set ⇒ p 0 ∈ K ∧ p 1 ∈ K) (b,k) Hbk) to the current goal.

Apply andI to the current goal.

rewrite the current goal using (tuple_2_0_eq b k) (from left to right).

An exact proof term for the current goal is HbK.

rewrite the current goal using (tuple_2_1_eq b k) (from left to right).

An exact proof term for the current goal is HkK.