Let x0 of type ι → ι → ο be given.
Apply and3E with
reflexive x0,
antisymmetric x0,
transitive x0,
strictpartialorder (λ x1 x2 . and (x0 x1 x2) (x1 = x2 ⟶ ∀ x3 : ο . x3)) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply andI with
irreflexive (λ x1 x2 . and (x0 x1 x2) (x1 = x2 ⟶ ∀ x3 : ο . x3)),
transitive (λ x1 x2 . and (x0 x1 x2) (x1 = x2 ⟶ ∀ x3 : ο . x3)) leaving 2 subgoals.
Let x1 of type ι be given.
Assume H4:
and (x0 x1 x1) (x1 = x1 ⟶ ∀ x2 : ο . x2).
Apply andER with
x0 x1 x1,
x1 = x1 ⟶ ∀ x2 : ο . x2 leaving 2 subgoals.
The subproof is completed by applying H4.
Let x2 of type ι → ι → ο be given.
Assume H5: x2 x1 x1.
The subproof is completed by applying H5.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Assume H4:
and (x0 x1 x2) (x1 = x2 ⟶ ∀ x4 : ο . x4).
Assume H5:
and (x0 x2 x3) (x2 = x3 ⟶ ∀ x4 : ο . x4).
Apply H4 with
and (x0 x1 x3) (x1 = x3 ⟶ ∀ x4 : ο . x4).
Assume H6: x0 x1 x2.
Assume H7: x1 = x2 ⟶ ∀ x4 : ο . x4.
Apply H5 with
and (x0 x1 x3) (x1 = x3 ⟶ ∀ x4 : ο . x4).
Assume H8: x0 x2 x3.
Assume H9: x2 = x3 ⟶ ∀ x4 : ο . x4.
Apply andI with
x0 x1 x3,
x1 = x3 ⟶ ∀ x4 : ο . x4 leaving 2 subgoals.
Apply H3 with
x1,
x2,
x3 leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H8.
Assume H10: x1 = x3.
Claim L11: x0 x2 x1
Apply H10 with
λ x4 x5 . x0 x2 x5.
The subproof is completed by applying H8.
Apply H7.
Apply H2 with
x1,
x2 leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying L11.