theorem :: TWOSCOMP:57

for x, y being Element of BOOLEAN holds nand2 . <*x,y*> = ('not' x) 'or' ('not' y) by Lm2;