let D1, D2 be non empty Subset-Family of Omega; :: thesis: ( ( for B being set holds
( B in D1 iff ( B in Sigma & B c= A & A \ B is thin of P ) ) ) & ( for B being set holds
( B in D2 iff ( B in Sigma & B c= A & A \ B is thin of P ) ) ) implies D1 = D2 )
assume that
A9: for B being set holds
( B in D1 iff ( B in Sigma & B c= A & A \ B is thin of P ) ) and
A10: for B being set holds
( B in D2 iff ( B in Sigma & B c= A & A \ B is thin of P ) ) ; :: thesis: D1 = D2
for B being set holds
( B in D1 iff B in D2 )

proof

let B be set ; :: thesis: ( B in D1 iff B in D2 )
thus ( B in D1 implies B in D2 ) :: thesis: ( B in D2 implies B in D1 )

proof

assume B in D1 ; :: thesis: B in D2
then ( B in Sigma & B c= A & A \ B is thin of P ) by A9;
hence B in D2 by A10; :: thesis: verum

end;

assume B in D2 ; :: thesis: B in D1
then ( B in Sigma & B c= A & A \ B is thin of P ) by A10;
hence B in D1 by A9; :: thesis: verum

end;

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