defpred S_{1}[ set ] means for t being set st t = $1 holds

( t in S & t c= A & A \ t is thin of M );

consider D being set such that

A1: for t being set holds

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

A2: for B being set holds

( B in D iff ( B in S & B c= A & A \ B is thin of M ) )

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

( B in D iff ( B in S & B c= A & A \ B is thin of M ) )

thus for B being set holds

( B in D iff ( B in S & B c= A & A \ B is thin of M ) ) by A2; :: thesis: verum

( t in S & t c= A & A \ t is thin of M );

consider D being set such that

A1: for t being set holds

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

A2: for B being set holds

( B in D iff ( B in S & B c= A & A \ B is thin of M ) )

proof

A5:
D c= bool X
let B be set ; :: thesis: ( B in D iff ( B in S & B c= A & A \ B is thin of M ) )

( B in S & B c= A & A \ B is thin of M implies B in D )

end;( B in S & B c= A & A \ B is thin of M implies B in D )

proof

hence
( B in D iff ( B in S & B c= A & A \ B is thin of M ) )
by A1; :: thesis: verum
assume that

A3: B in S and

A4: ( B c= A & A \ B is thin of M ) ; :: thesis: B in D

for t being set st t = B holds

( t in S & t c= A & A \ t is thin of M ) by A3, A4;

hence B in D by A1, A3; :: thesis: verum

end;A3: B in S and

A4: ( B c= A & A \ B is thin of M ) ; :: thesis: B in D

for t being set st t = B holds

( t in S & t c= A & A \ t is thin of M ) by A3, A4;

hence B in D by A1, A3; :: thesis: verum

proof

D <> {}
let B be object ; :: according to TARSKI:def 3 :: thesis: ( not B in D or B in bool X )

assume B in D ; :: thesis: B in bool X

then B in S by A2;

hence B in bool X ; :: thesis: verum

end;assume B in D ; :: thesis: B in bool X

then B in S by A2;

hence B in bool X ; :: thesis: verum

proof

then reconsider D = D as non empty Subset-Family of X by A5;
consider B being set such that

A6: B in S and

A7: ex C being thin of M st A = B \/ C by Def3;

consider C being thin of M such that

A8: A = B \/ C by A7;

consider E being set such that

A9: E in S and

A10: C c= E and

A11: M . E = 0. by Def2;

A \ B = C \ B by A8, XBOOLE_1:40;

then A \ B c= C by XBOOLE_1:36;

then A \ B c= E by A10;

then A12: A \ B is thin of M by A9, A11, Def2;

B c= A by A8, XBOOLE_1:7;

hence D <> {} by A2, A6, A12; :: thesis: verum

end;A6: B in S and

A7: ex C being thin of M st A = B \/ C by Def3;

consider C being thin of M such that

A8: A = B \/ C by A7;

consider E being set such that

A9: E in S and

A10: C c= E and

A11: M . E = 0. by Def2;

A \ B = C \ B by A8, XBOOLE_1:40;

then A \ B c= C by XBOOLE_1:36;

then A \ B c= E by A10;

then A12: A \ B is thin of M by A9, A11, Def2;

B c= A by A8, XBOOLE_1:7;

hence D <> {} by A2, A6, A12; :: thesis: verum

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

( B in D iff ( B in S & B c= A & A \ B is thin of M ) )

thus for B being set holds

( B in D iff ( B in S & B c= A & A \ B is thin of M ) ) by A2; :: thesis: verum