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 A7: 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 A7;
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 A7; :: thesis: verum