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