let D1, D2 be non empty Subset-Family of Omega; :: thesis: ( ( for A being set holds
( A in D1 iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) ) ) & ( for A being set holds
( A in D2 iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) ) ) implies D1 = D2 )
assume that
A12: for A being set holds
( A in D1 iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) ) and
A13: for A being set holds
( A in D2 iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) ) ; :: thesis: D1 = D2
for A being set holds
( A in D1 iff A in D2 )

proof

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

proof

assume A in D1 ; :: thesis: A in D2
then ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) by A12;
hence A in D2 by A13; :: thesis: verum

end;

assume A in D2 ; :: thesis: A in D1
then ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) by A13;
hence A in D1 by A12; :: thesis: verum

end;

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