reconsider a = {} as Subset of (union C) by XBOOLE_1:2;
then
a in 'not' C
;
hence
not 'not' C is empty
; ( 'not' C is subset-closed & 'not' C is binary_complete )
let A be set ; COHSP_1:def 1 ( ( for a, b being set st a in A & b in A holds
a \/ b in 'not' C ) implies union A in 'not' C )
assume A5:
for a, b being set st a in A & b in A holds
a \/ b in 'not' C
; union A in 'not' C
A c= bool (union C)
then
union A c= union (bool (union C))
by ZFMISC_1:77;
then reconsider a = union A as Subset of (union C) by ZFMISC_1:81;
now for c being Element of C ex x being set st a /\ c c= {x}let c be
Element of
C;
ex x being set st a /\ x c= {b2}per cases
( a /\ c = {} or a /\ c <> {} )
;
suppose
a /\ c <> {}
;
ex y being set st a /\ y c= {b2}then reconsider X =
a /\ c as non
empty set ;
set x = the
Element of
X;
reconsider y = the
Element of
X as
set ;
take y =
y;
a /\ c c= {y}thus
a /\ c c= {y}
verumproof
let z be
object ;
TARSKI:def 3 ( not z in a /\ c or z in {y} )
assume A7:
z in a /\ c
;
z in {y}
then A8:
z in c
by XBOOLE_0:def 4;
the
Element of
X in a
by XBOOLE_0:def 4;
then consider w being
set such that A9:
the
Element of
X in w
and A10:
w in A
by TARSKI:def 4;
z in a
by A7, XBOOLE_0:def 4;
then consider v being
set such that A11:
z in v
and A12:
v in A
by TARSKI:def 4;
w \/ v in 'not' C
by A5, A12, A10;
then consider aa being
Subset of
(union C) such that A13:
w \/ v = aa
and A14:
for
b being
Element of
C ex
x being
set st
aa /\ b c= {x}
;
consider t being
set such that A15:
aa /\ c c= {t}
by A14;
( the
Element of
X in c & the
Element of
X in aa )
by A9, A13, XBOOLE_0:def 3, XBOOLE_0:def 4;
then A16:
the
Element of
X in aa /\ c
by XBOOLE_0:def 4;
z in aa
by A11, A13, XBOOLE_0:def 3;
then
z in aa /\ c
by A8, XBOOLE_0:def 4;
then
z in {t}
by A15;
hence
z in {y}
by A15, A16, TARSKI:def 1;
verum
end; end; end;
hence
union A in 'not' C
; verum