Let J and le be given.
Assume Hpo: partial_order_on J le.
We will prove ∀a b : set, a ∈ J → b ∈ J → (a,b) ∈ le → (b,a) ∈ le → a = b.
Let a and b be given.
Assume HaJ: a ∈ J.
Assume HbJ: b ∈ J.
Assume Hab: (a,b) ∈ le.
Assume Hba: (b,a) ∈ le.
We prove the intermediate claim Htmp: (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 Hantisym: ∀a0 b0 : set, a0 ∈ J → b0 ∈ J → (a0,b0) ∈ le → (b0,a0) ∈ le → a0 = b0.
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) Htmp).
An exact proof term for the current goal is (Hantisym a b HaJ HbJ Hab Hba).
∎