Proofgold Proof

pf
Apply andI with strictpartialorder ZermeloWOstrict, trichotomous_or ZermeloWOstrict leaving 2 subgoals. Apply partialorder_strictpartialorder with ZermeloWO. The subproof is completed by applying ZermeloWO_partialorder. The subproof is completed by applying ZermeloWOstrict_trich. ■