theorem :: XBOOLEAN:87

for p, q being boolean object holds ('not' p) 'xor' (q => p) = (p '&' (p 'or' ('not' q))) 'or' (('not' p) '&' q)