:: deftheorem defines TVERUM LTLAXIO1:def 3 :
TVERUM = 'not' TFALSUM;