:: deftheorem defines 'or' XBOOLEAN:def 6 :
for p, q being boolean object holds p 'or' q = 'not' (('not' p) '&' ('not' q));