theorem :: XBOOLEAN:56

for p, q being boolean object holds p => (p 'nand' q) = p 'nand' q