:: deftheorem Def14 defines nand3b TWOSCOMP:def 14 :
for b₁ being Function of (3 -tuples_on BOOLEAN),BOOLEAN holds
( b₁ = nand3b iff for x, y, z being Element of BOOLEAN holds b₁ . <*x,y,z*> = 'not' ((('not' x) '&' ('not' y)) '&' z) );