Proofgold Proof

pf
Apply and3I with reflexive ZermeloWO, antisymmetric ZermeloWO, transitive ZermeloWO leaving 3 subgoals. The subproof is completed by applying ZermeloWO_ref. The subproof is completed by applying ZermeloWO_antisym. The subproof is completed by applying ZermeloWO_tra. ■