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 ) )

( X in SFY & Y in SFX & Z = X /\ Y ) implies Z in SFZ ) by A14; :: thesis: verum

( 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 )

thus
( 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;( 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

( X in SFY & Y in SFX & Z = X /\ Y ) implies Z in SFZ ) by A14; :: thesis: verum