Proofgold Proof

pf
Apply andI with partialorder ZermeloWO, linear ZermeloWO leaving 2 subgoals. The subproof is completed by applying ZermeloWO_partialorder. The subproof is completed by applying ZermeloWO_lin. ■