theorem :: XBOOLEAN:63

for p, q being boolean object holds ('not' p) '&' (p 'nand' q) = ('not' p) 'or' (('not' p) '&' ('not' q))