theorem :: BVFUNC25:54

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