defpred S1[ 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
A15: for x being set holds
( x in XX iff ( x in bool (union SFX) & S1[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 ) )
A16: 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 A17: X in SFX and
A18: Y in SFY and
A19: Z = X \ Y ; :: thesis: Z in XX
X c= union SFX by A17, ZFMISC_1:74;
then Z c= union SFX by A19;
hence Z in XX by A15, A17, A18, A19; :: 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 A15;
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 A16; :: 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