let D1, D2 be non empty Subset-Family of X; :: thesis: ( ( for A being set holds
( A in D1 iff ex B being set st
( B in S & ex C being thin of M st A = B \/ C ) ) ) & ( for A being set holds
( A in D2 iff ex B being set st
( B in S & ex C being thin of M st A = B \/ C ) ) ) implies D1 = D2 )
assume that
A13: for A being set holds
( A in D1 iff ex B being set st
( B in S & ex C being thin of M st A = B \/ C ) ) and
A14: for A being set holds
( A in D2 iff ex B being set st
( B in S & ex C being thin of M 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 S & ex C being thin of M st A = B \/ C ) by A13;
hence A in D2 by A14; :: thesis: verum

end;

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

end;

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