:: deftheorem defines 'xor' XBOOLEAN:def 11 :
for p, q being boolean object holds p 'xor' q = 'not' (p <=> q);