theorem Th1: :: BVFUNC_1:2

for Y being non empty set holds
( 'not' (I_el Y) = O_el Y & 'not' (O_el Y) = I_el Y )