let D1, D2 be non empty Subset-Family of Omega; ( ( 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
A11:
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
A12:
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 ) )
; D1 = D2
for A being object holds
( A in D1 iff A in D2 )
proof
let A be
object ;
( A in D1 iff A in D2 )
thus
(
A in D1 implies
A in D2 )
( A in D2 implies A in D1 )proof
assume
A in D1
;
A in D2
then
ex
B being
set st
(
B in Sigma & ex
C being
thin of
P st
A = B \/ C )
by A11;
hence
A in D2
by A12;
verum
end;
assume
A in D2
;
A in D1
then
ex
B being
set st
(
B in Sigma & ex
C being
thin of
P st
A = B \/ C )
by A12;
hence
A in D1
by A11;
verum
end;
hence
D1 = D2
by TARSKI:2; verum