theorem Th18: :: BVFUNC_1:19

for Y being non empty set
for a being Function of Y,BOOLEAN holds
( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) )