Let x0 of type ο be given.
Assume H0:
∀ x1 : ι → ι → ο . and (totalorder x1) (∀ x2 : ι → ο . (∃ x3 . x2 x3) ⟶ ∃ x3 . and (x2 x3) (∀ x4 . x2 x4 ⟶ x1 x3 x4)) ⟶ x0.
Apply H0 with
ZermeloWO.
Apply andI with
totalorder ZermeloWO,
∀ x1 : ι → ο . (∃ x2 . x1 x2) ⟶ ∃ x2 . and (x1 x2) (∀ x3 . x1 x3 ⟶ ZermeloWO x2 x3) leaving 2 subgoals.
The subproof is completed by applying ZermeloWO_totalorder.
The subproof is completed by applying ZermeloWO_wo.