defpred S₁[ set ] means ex Z being set st
( $1 = Z & ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) );
consider XX being set such that
A1: for x being set holds
( x in XX iff ( x in bool ((union SFX) \/ (union SFY)) & S₁[x] ) ) from XFAMILY:sch 1();
take XX ; :: thesis: for Z being set holds
( Z in XX iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) )
for Z being set holds
( Z in XX iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) )

proof

let Z be set ; :: thesis: ( Z in XX iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) )

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

given X, Y being set such that A3: ( X in SFX & Y in SFY ) and
A4: Z = X \/ Y ; :: thesis: Z in XX
( X c= union SFX & Y c= union SFY ) by A3, ZFMISC_1:74;
then Z c= (union SFX) \/ (union SFY) by A4, XBOOLE_1:13;
hence Z in XX by A1, A3, A4; :: thesis: verum

end;

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

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

end;

hence ( Z in XX iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) ) by A2; :: thesis: verum

end;

hence for Z being set holds
( Z in XX iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) ) ; :: thesis: verum