theorem :: BVFUNC25:65

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds
( a 'nand' (a 'nand' b) = ('not' a) 'or' b & a 'nand' (a 'nand' b) = a 'imp' b )