let X be set ; :: thesis: ( 'not' (FlatCoh X) = bool X & 'not' (bool X) = FlatCoh X )
thus 'not' (FlatCoh X) = bool X :: thesis: 'not' (bool X) = FlatCoh X

proof

hereby :: according to XBOOLE_0:def 10,TARSKI:def 3 :: thesis: bool X c= 'not' (FlatCoh X)

let x be set ; :: thesis: ( x in 'not' (FlatCoh X) implies x in bool X )
assume x in 'not' (FlatCoh X) ; :: thesis: x in bool X
then x c= union (FlatCoh X) by Th66;
then x c= X by Th2;
hence x in bool X ; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in bool X or x in 'not' (FlatCoh X) )
assume x in bool X ; :: thesis: x in 'not' (FlatCoh X)
then x c= X ;
then A1: x c= union (FlatCoh X) by Th2;

now

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

per cases ( a = {} or ex z being set st
( a = {z} & z in X ) ) by Th1;

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

then x /\ a c= {0 } by XBOOLE_1:2;
hence ex z being set st x /\ a c= {z} ; :: thesis: verum

end;

suppose ex z being set st
( a = {z} & z in X ) ; :: thesis: ex z being set st x /\ z c= {b₂}

then consider z being set such that
A2: ( a = {z} & z in X ) ;
take z = z; :: thesis: x /\ a c= {z}
thus x /\ a c= {z} by A2, XBOOLE_1:17; :: thesis: verum

end;

end;

end;

hence x in 'not' (FlatCoh X) by A1; :: thesis: verum

end;

hence 'not' (bool X) = FlatCoh X by Th71; :: thesis: verum