theorem :: XBOOLEAN:42

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