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