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 )

( 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

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

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;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 A17:
B in D2
; :: thesis: B in D1
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;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

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