A1:
ex B being set st

( B in S & {} c= B & M . B = 0. )

A4: for A being set st A = {} holds

ex B being set st

( B in S & ex C being thin of M st A = B \/ C )_{1}[ set ] means for A being set st A = $1 holds

ex B being set st

( B in S & ex C being thin of M st A = B \/ C );

consider D being set such that

A7: for y being set holds

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

A8: for A being set holds

( A in D iff ex B being set st

( B in S & ex C being thin of M st A = B \/ C ) )

{} c= X ;

then reconsider D = D as non empty Subset-Family of X by A7, A11, A4;

take D ; :: thesis: for A being set holds

( A in D iff ex B being set st

( B in S & ex C being thin of M st A = B \/ C ) )

thus for A being set holds

( A in D iff ex B being set st

( B in S & ex C being thin of M st A = B \/ C ) ) by A8; :: thesis: verum

( B in S & {} c= B & M . B = 0. )

proof

A3:
{} is Subset of X
by XBOOLE_1:2;
consider B being set such that

A2: ( B = {} & B in S ) by PROB_1:4;

take B ; :: thesis: ( B in S & {} c= B & M . B = 0. )

thus ( B in S & {} c= B & M . B = 0. ) by A2, VALUED_0:def 19; :: thesis: verum

end;A2: ( B = {} & B in S ) by PROB_1:4;

take B ; :: thesis: ( B in S & {} c= B & M . B = 0. )

thus ( B in S & {} c= B & M . B = 0. ) by A2, VALUED_0:def 19; :: thesis: verum

A4: for A being set st A = {} holds

ex B being set st

( B in S & ex C being thin of M st A = B \/ C )

proof

defpred S
reconsider C = {} as thin of M by A3, A1, Def2;

let A be set ; :: thesis: ( A = {} implies ex B being set st

( B in S & ex C being thin of M st A = B \/ C ) )

consider B being set such that

A5: B = {} and

A6: B in S by PROB_1:4;

assume A = {} ; :: thesis: ex B being set st

( B in S & ex C being thin of M st A = B \/ C )

then A = B \/ C by A5;

hence ex B being set st

( B in S & ex C being thin of M st A = B \/ C ) by A6; :: thesis: verum

end;let A be set ; :: thesis: ( A = {} implies ex B being set st

( B in S & ex C being thin of M st A = B \/ C ) )

consider B being set such that

A5: B = {} and

A6: B in S by PROB_1:4;

assume A = {} ; :: thesis: ex B being set st

( B in S & ex C being thin of M st A = B \/ C )

then A = B \/ C by A5;

hence ex B being set st

( B in S & ex C being thin of M st A = B \/ C ) by A6; :: thesis: verum

ex B being set st

( B in S & ex C being thin of M st A = B \/ C );

consider D being set such that

A7: for y being set holds

( y in D iff ( y in bool X & S

A8: for A being set holds

( A in D iff ex B being set st

( B in S & ex C being thin of M st A = B \/ C ) )

proof

A11:
D c= bool X
by A7;
let A be set ; :: thesis: ( A in D iff ex B being set st

( B in S & ex C being thin of M st A = B \/ C ) )

A9: ( A in D iff ( A in bool X & ( for y being set st y = A holds

ex B being set st

( B in S & ex C being thin of M st y = B \/ C ) ) ) ) by A7;

( ex B being set st

( B in S & ex C being thin of M st A = B \/ C ) implies A in D )

( B in S & ex C being thin of M st A = B \/ C ) ) by A7; :: thesis: verum

end;( B in S & ex C being thin of M st A = B \/ C ) )

A9: ( A in D iff ( A in bool X & ( for y being set st y = A holds

ex B being set st

( B in S & ex C being thin of M st y = B \/ C ) ) ) ) by A7;

( ex B being set st

( B in S & ex C being thin of M st A = B \/ C ) implies A in D )

proof

hence
( A in D iff ex B being set st
assume A10:
ex B being set st

( B in S & ex C being thin of M st A = B \/ C ) ; :: thesis: A in D

then A c= X by XBOOLE_1:8;

hence A in D by A9, A10; :: thesis: verum

end;( B in S & ex C being thin of M st A = B \/ C ) ; :: thesis: A in D

then A c= X by XBOOLE_1:8;

hence A in D by A9, A10; :: thesis: verum

( B in S & ex C being thin of M st A = B \/ C ) ) by A7; :: thesis: verum

{} c= X ;

then reconsider D = D as non empty Subset-Family of X by A7, A11, A4;

take D ; :: thesis: for A being set holds

( A in D iff ex B being set st

( B in S & ex C being thin of M st A = B \/ C ) )

thus for A being set holds

( A in D iff ex B being set st

( B in S & ex C being thin of M st A = B \/ C ) ) by A8; :: thesis: verum