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

A12: 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

A13: 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 object holds

( A in D1 iff A in D2 )

( 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

A12: 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

A13: 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 object holds

( A in D1 iff A in D2 )

proof

hence
D1 = D2
by TARSKI:2; :: thesis: verum
let A be object ; :: thesis: ( A in D1 iff A in D2 )

thus ( A in D1 implies A in D2 ) :: thesis: ( A in D2 implies A in D1 )

then ex B being set st

( B in S & ex C being thin of M st A = B \/ C ) by A13;

hence A in D1 by A12; :: thesis: verum

end;thus ( A in D1 implies A in D2 ) :: thesis: ( A in D2 implies A in D1 )

proof

assume
A in D2
; :: thesis: A in D1
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 A12;

hence A in D2 by A13; :: thesis: verum

end;then ex B being set st

( B in S & ex C being thin of M st A = B \/ C ) by A12;

hence A in D2 by A13; :: thesis: verum

then ex B being set st

( B in S & ex C being thin of M st A = B \/ C ) by A13;

hence A in D1 by A12; :: thesis: verum