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 object ; :: thesis: ( x in 'not' (FlatCoh X) implies x in bool X )
reconsider xx = x as set by TARSKI:1;
assume x in 'not' (FlatCoh X) ; :: thesis: x in bool X
then xx c= union (FlatCoh X) by Th65;
then xx c= X by Th2;
hence x in bool X ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in bool X or x in 'not' (FlatCoh X) )
reconsider xx = x as set by TARSKI:1;
A1: now :: thesis: for a being Element of FlatCoh X ex z being set st xx /\ a c= {z}
let a be Element of FlatCoh X; :: thesis: ex z being set st xx /\ z c= {b2}
per cases ( a = {} or ex z being set st
( a = {z} & z in X ) ) by Th1;
suppose a = {} ; :: thesis: ex z being set st xx /\ z c= {b2}
then xx /\ a c= {0} ;
hence ex z being set st xx /\ a c= {z} ; :: thesis: verum
end;
suppose ex z being set st
( a = {z} & z in X ) ; :: thesis: ex z being set st xx /\ z c= {b2}
then consider z being set such that
A2: a = {z} and
z in X ;
take z = z; :: thesis: xx /\ a c= {z}
thus xx /\ a c= {z} by A2, XBOOLE_1:17; :: thesis: verum
end;
end;
end;
assume x in bool X ; :: thesis: x in 'not' (FlatCoh X)
then xx c= X ;
then xx c= union (FlatCoh X) by Th2;
hence x in 'not' (FlatCoh X) by A1; :: thesis: verum
end;
hence 'not' (bool X) = FlatCoh X by Th70; :: thesis: verum