Let J and le be given.
Assume Hpo: partial_order_on J le.
We will prove ∀a b c : set, a ∈ J → b ∈ J → c ∈ J → (a,b) ∈ le → (b,c) ∈ le → (a,c) ∈ le.
Let a, b and c be given.
Assume HaJ: a ∈ J.
Assume HbJ: b ∈ J.
Assume HcJ: c ∈ J.
Assume Hab: (a,b) ∈ le.
Assume Hbc: (b,c) ∈ le.
We prove the intermediate claim Hleft: ((relation_on le J ∧ (∀a0 : set, a0 ∈ J → (a0,a0) ∈ le)) ∧ (∀a0 b0 : set, a0 ∈ J → b0 ∈ J → (a0,b0) ∈ le → (b0,a0) ∈ le → a0 = b0)).
An exact proof term for the current goal is (andEL ((relation_on le J ∧ (∀a0 : set, a0 ∈ J → (a0,a0) ∈ le)) ∧ (∀a0 b0 : set, a0 ∈ J → b0 ∈ J → (a0,b0) ∈ le → (b0,a0) ∈ le → a0 = b0)) (∀a0 b0 c0 : set, a0 ∈ J → b0 ∈ J → c0 ∈ J → (a0,b0) ∈ le → (b0,c0) ∈ le → (a0,c0) ∈ le) Hpo).
We prove the intermediate claim Htrans: ∀a0 b0 c0 : set, a0 ∈ J → b0 ∈ J → c0 ∈ J → (a0,b0) ∈ le → (b0,c0) ∈ le → (a0,c0) ∈ le.
An exact proof term for the current goal is (andER ((relation_on le J ∧ (∀a0 : set, a0 ∈ J → (a0,a0) ∈ le)) ∧ (∀a0 b0 : set, a0 ∈ J → b0 ∈ J → (a0,b0) ∈ le → (b0,a0) ∈ le → a0 = b0)) (∀a0 b0 c0 : set, a0 ∈ J → b0 ∈ J → c0 ∈ J → (a0,b0) ∈ le → (b0,c0) ∈ le → (a0,c0) ∈ le) Hpo).
An exact proof term for the current goal is (Htrans a b c HaJ HbJ HcJ Hab Hbc).
∎