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