defpred S_{1}[ set ] means ex Z being set st

( $1 = Z & P_{1}[Z] );

consider X being set such that

A2: for x being set holds

( x in X iff ( x in bool F_{1}() & S_{1}[x] ) )
from XFAMILY:sch 1();

X c= bool F_{1}()
by A2;

then reconsider X = X as non empty Subset-Family of F_{1}() by A1, A2;

take X ; :: thesis: for B being set holds

( B in X iff ( B c= F_{1}() & P_{1}[B] ) )

for B being set holds

( B in X iff ( B c= F_{1}() & P_{1}[B] ) )

( B in X iff ( B c= F_{1}() & P_{1}[B] ) )
; :: thesis: verum

( $1 = Z & P

consider X being set such that

A2: for x being set holds

( x in X iff ( x in bool F

X c= bool F

then reconsider X = X as non empty Subset-Family of F

take X ; :: thesis: for B being set holds

( B in X iff ( B c= F

for B being set holds

( B in X iff ( B c= F

proof

hence
for B being set holds
let B be set ; :: thesis: ( B in X iff ( B c= F_{1}() & P_{1}[B] ) )

thus ( B in X implies ( B c= F_{1}() & P_{1}[B] ) )
:: thesis: ( B c= F_{1}() & P_{1}[B] implies B in X )_{1}() & P_{1}[B] )
; :: thesis: B in X

hence B in X by A2; :: thesis: verum

end;thus ( B in X implies ( B c= F

proof

assume
( B c= F
assume A3:
B in X
; :: thesis: ( B c= F_{1}() & P_{1}[B] )

then ex Z being set st

( B = Z & P_{1}[Z] )
by A2;

hence ( B c= F_{1}() & P_{1}[B] )
by A3; :: thesis: verum

end;then ex Z being set st

( B = Z & P

hence ( B c= F

hence B in X by A2; :: thesis: verum

( B in X iff ( B c= F