let D1, D2 be non empty Subset-Family of X; :: thesis: ( ( for B being set holds
( B in D1 iff ( B in S & B c= A & A \ B is thin of M ) ) ) & ( for B being set holds
( B in D2 iff ( B in S & B c= A & A \ B is thin of M ) ) ) implies D1 = D2 )
assume that
A13: for B being set holds
( B in D1 iff ( B in S & B c= A & A \ B is thin of M ) ) and
A14: for B being set holds
( B in D2 iff ( B in S & B c= A & A \ B is thin of M ) ) ; :: thesis: D1 = D2
for B being object holds
( B in D1 iff B in D2 )

proof

let B be object ; :: thesis: ( B in D1 iff B in D2 )
reconsider BB = B as set by TARSKI:1;
thus ( B in D1 implies B in D2 ) :: thesis: ( B in D2 implies B in D1 )

proof

assume A15: B in D1 ; :: thesis: B in D2
then A16: A \ BB is thin of M by A13;
( B in S & BB c= A ) by A13, A15;
hence B in D2 by A14, A16; :: thesis: verum

end;

assume A17: B in D2 ; :: thesis: B in D1
then A18: A \ BB is thin of M by A14;
( B in S & BB c= A ) by A14, A17;
hence B in D1 by A13, A18; :: thesis: verum

end;

hence D1 = D2 by TARSKI:2; :: thesis: verum