theorem :: COHSP_1:72

for X being set holds
( 'not' (FlatCoh X) = bool X & 'not' (bool X) = FlatCoh X )