let SFZ, SFX, SFY be set ; :: thesis: ( ( for Z being set holds
( Z in SFZ iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) ) ) implies for Z being set holds
( Z in SFZ iff ex X, Y being set st
( X in SFY & Y in SFX & Z = X /\ Y ) ) )
assume A14: for Z being set holds
( Z in SFZ iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) ) ; :: thesis: for Z being set holds
( Z in SFZ iff ex X, Y being set st
( X in SFY & Y in SFX & Z = X /\ Y ) )
let Z be set ; :: thesis: ( Z in SFZ iff ex X, Y being set st
( X in SFY & Y in SFX & Z = X /\ Y ) )

hereby :: thesis: ( ex X, Y being set st
( X in SFY & Y in SFX & Z = X /\ Y ) implies Z in SFZ )

assume Z in SFZ ; :: thesis: ex Y, X being set st
( Y in SFY & X in SFX & Z = Y /\ X )
then ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) by A14;
hence ex Y, X being set st
( Y in SFY & X in SFX & Z = Y /\ X ) ; :: thesis: verum

end;

thus ( ex X, Y being set st
( X in SFY & Y in SFX & Z = X /\ Y ) implies Z in SFZ ) by A14; :: thesis: verum