:: deftheorem defines 'not' LTLAXIO1:def 1 :
for p being Element of LTLB_WFF holds 'not' p = p => TFALSUM;