theorem :: XBOOLEAN:85
for p, q being boolean object holds p => (p 'xor' q) = ('not' p) 'or' ('not' q)