defpred S_{1}[ 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

A8: for x being set holds

( x in XX iff ( x in bool ((union SFX) /\ (union SFY)) & S_{1}[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 ) )

( Z in XX iff ex X, Y being set st

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

( $1 = Z & ex X, Y being set st

( X in SFX & Y in SFY & Z = X /\ Y ) );

consider XX being set such that

A8: for x being set holds

( x in XX iff ( x in bool ((union SFX) /\ (union SFY)) & S

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

hence
for Z being set holds
let Z be set ; :: thesis: ( Z in XX iff ex X, Y being set st

( X in SFX & Y in SFY & Z = X /\ Y ) )

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

end;( X in SFX & Y in SFY & Z = X /\ Y ) )

A9: now :: thesis: ( ex X, Y being set st

( X in SFX & Y in SFY & Z = X /\ Y ) implies Z in XX )

( X in SFX & Y in SFY & Z = X /\ Y ) implies Z in XX )

given X, Y being set such that A10:
( X in SFX & Y in SFY )
and

A11: Z = X /\ Y ; :: thesis: Z in XX

( X c= union SFX & Y c= union SFY ) by A10, ZFMISC_1:74;

then Z c= (union SFX) /\ (union SFY) by A11, XBOOLE_1:27;

hence Z in XX by A8, A10, A11; :: thesis: verum

end;A11: Z = X /\ Y ; :: thesis: Z in XX

( X c= union SFX & Y c= union SFY ) by A10, ZFMISC_1:74;

then Z c= (union SFX) /\ (union SFY) by A11, XBOOLE_1:27;

hence Z in XX by A8, A10, A11; :: thesis: verum

now :: thesis: ( Z in XX implies ex X, Y being set st

( X in SFX & Y in SFY & Z = X /\ Y ) )

hence
( Z in XX iff 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 A8;

hence ex X, Y being set st

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

end;( 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 A8;

hence ex X, Y being set st

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

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

( Z in XX iff ex X, Y being set st

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