:: deftheorem Def3 defines 'nand' BVFUNC25:def 3 :
for A being non empty set
for p, q, b₄ being Function of A,BOOLEAN holds
( b₄ = p 'nand' q iff for x being Element of A holds b₄ . x = (p . x) 'nand' (q . x) );