:: deftheorem defines 'not' XBOOLEAN:def 4 :
for p being boolean object holds 'not' p = 1 - p;