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

( X in SFY & Y in SFX & Z = X \/ Y ) implies Z in SFZ ) by A7; :: 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 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 )

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 A7;

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 A7;

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