theorem :: BVFUNC25:77

for Y being non empty set
for a being Function of Y,BOOLEAN holds
( a 'nor' ('not' a) = O_el Y & 'not' (a 'nor' ('not' a)) = I_el Y )