Let x0 of type ο be given.
Assume H0:
∀ x1 : ι → ι → ο . and (stricttotalorder x1) (∀ x2 : ι → ο . (∃ x3 . x2 x3) ⟶ ∃ x3 . and (x2 x3) (∀ x4 . and (x2 x4) (x4 = x3 ⟶ ∀ x5 : ο . x5) ⟶ x1 x3 x4)) ⟶ x0.
Apply H0 with
ZermeloWOstrict.
Apply andI with
stricttotalorder ZermeloWOstrict,
∀ x1 : ι → ο . (∃ x2 . x1 x2) ⟶ ∃ x2 . and (x1 x2) (∀ x3 . and (x1 x3) (x3 = x2 ⟶ ∀ x4 : ο . x4) ⟶ ZermeloWOstrict x2 x3) leaving 2 subgoals.
The subproof is completed by applying ZermeloWOstrict_stricttotalorder.
The subproof is completed by applying ZermeloWOstrict_wo.