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 ;
hence B in D2 by ; :: 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 ;
hence B in D1 by ; :: thesis: verum
end;
hence D1 = D2 by TARSKI:2; :: thesis: verum