Proofgold Proof

pf
Let x0 of type ι be given. Let x1 of type ι be given. Let x2 of type ι be given. The subproof is completed by applying and3E with subfield x0 x1, x2 ∈ setminus (field0 x1) (field0 x0), ∀ x3 . subfield x0 x3 ⟶ x2 ∈ field0 x3 ⟶ subfield x1 x3. ■