theorem :: BVFUNC_1:43

for x being boolean object holds TRUE 'nand' x = 'not' x ;