theorem :: BVFUNC_1:45

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