:: deftheorem Def2 defines nand2 TWOSCOMP:def 2 :
for b₁ being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds
( b₁ = nand2 iff for x, y being Element of BOOLEAN holds b₁ . <*x,y*> = 'not' (x '&' y) );