theorem :: BVFUNC_1:46

for x, y being boolean object holds 'not' (x 'nand' y) = x '&' y ;