reconsider a = {} as Subset of (union C) by XBOOLE_1:2;

now :: thesis: for b being Element of C ex x being set st a /\ b c= {x}

let b be Element of C; :: thesis: ex x being set st a /\ b c= {x}
take x = {} ; :: thesis: a /\ b c= {x}
thus a /\ b c= {x} ; :: thesis: verum

end;

then a in 'not' C ;
hence not 'not' C is empty ; :: thesis: ( 'not' C is subset-closed & 'not' C is binary_complete )

hereby :: according to CLASSES1:def 1 :: thesis: 'not' C is binary_complete

let a, b be set ; :: thesis: ( a in 'not' C & b c= a implies b in 'not' C )
assume a in 'not' C ; :: thesis: ( b c= a implies b in 'not' C )
then consider aa being Subset of (union C) such that
A1: a = aa and
A2: for b being Element of C ex x being set st aa /\ b c= {x} ;
assume A3: b c= a ; :: thesis: b in 'not' C
then reconsider bb = b as Subset of (union C) by A1, XBOOLE_1:1;

now :: thesis: for c being Element of C ex x being set st bb /\ c c= {x}

let c be Element of C; :: thesis: ex x being set st bb /\ c c= {x}
consider x being set such that
A4: aa /\ c c= {x} by A2;
take x = x; :: thesis: bb /\ c c= {x}
b /\ c c= a /\ c by A3, XBOOLE_1:26;
hence bb /\ c c= {x} by A1, A4; :: thesis: verum

end;

hence b in 'not' C ; :: thesis: verum

end;

let A be set ; :: according to COHSP_1:def 1 :: thesis: ( ( 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 ; :: thesis: union A in 'not' C
A c= bool (union C)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in bool (union C) )
reconsider xx = x as set by TARSKI:1;
assume x in A ; :: thesis: x in bool (union C)
then xx \/ xx in 'not' C by A5;
then ex a being Subset of (union C) st
( x = a & ( for b being Element of C ex x being set st a /\ b c= {x} ) ) ;
hence x in bool (union C) ; :: thesis: verum

end;

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 :: thesis: for c being Element of C ex x being set st a /\ c c= {x}

let c be Element of C; :: thesis: ex x being set st a /\ x c= {b₂}

per cases ( a /\ c = {} or a /\ c <> {} ) ;

suppose A6: a /\ c = {} ; :: thesis: ex x being set st a /\ x c= {b₂}

take x = {} ; :: thesis: a /\ c c= {x}
thus a /\ c c= {x} by A6; :: thesis: verum

end;

suppose a /\ c <> {} ; :: thesis: ex y being set st a /\ y c= {b₂}

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; :: thesis: a /\ c c= {y}
thus a /\ c c= {y} :: thesis: verum

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in a /\ c or z in {y} )
assume A7: z in a /\ c ; :: thesis: 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; :: thesis: verum

end;

end;

end;

end;

hence union A in 'not' C ; :: thesis: verum