theorem :: XBOOLEAN:37

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