theorem :: BVFUNC25:75

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