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

now

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} by XBOOLE_1:2; :: 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 & ( for b being Element of C ex x being set st aa /\ b c= {x} ) ) ;
assume A2: b c= a ; :: thesis: b in 'not' C
then reconsider bb = b as Subset of (union C) by A1, XBOOLE_1:1;

now

let c be Element of C; :: thesis: ex x being set st bb /\ c c= {x}
consider x being set such that
A3: aa /\ c c= {x} by A1;
take x = x; :: thesis: bb /\ c c= {x}
b /\ c c= a /\ c by A2, XBOOLE_1:26;
hence bb /\ c c= {x} by A1, A3, XBOOLE_1:1; :: 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 A4: 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 set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in bool (union C) )
assume x in A ; :: thesis: x in bool (union C)
then x \/ x in 'not' C by A4;
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:95;
then reconsider a = union A as Subset of (union C) by ZFMISC_1:99;

now

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

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

suppose A5: 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 A5, XBOOLE_1:2; :: 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 ;
consider x being Element of X;
reconsider y = x as set ;
take y = y; :: thesis: a /\ c c= {y}
thus a /\ c c= {y} :: thesis: verum

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in a /\ c or z in {y} )
assume z in a /\ c ; :: thesis: z in {y}
then A6: ( z in a & z in c ) by XBOOLE_0:def 4;
then consider v being set such that
A7: ( z in v & v in A ) by TARSKI:def 4;
A8: ( x in a & x in c ) by XBOOLE_0:def 4;
then consider w being set such that
A9: ( x in w & w in A ) by TARSKI:def 4;
w \/ v in 'not' C by A4, A7, A9;
then consider aa being Subset of (union C) such that
A10: ( w \/ v = aa & ( for b being Element of C ex x being set st aa /\ b c= {x} ) ) ;
consider t being set such that
A11: aa /\ c c= {t} by A10;
( z in aa & x in aa ) by A7, A9, A10, XBOOLE_0:def 3;
then ( z in aa /\ c & x in aa /\ c ) by A6, A8, XBOOLE_0:def 4;
then ( z in {t} & x in {t} ) by A11;
hence z in {y} by TARSKI:def 1; :: thesis: verum

end;

end;

end;

end;

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