:: deftheorem defines 'X' LTLAXIO1:def 2 :
for p being Element of LTLB_WFF holds 'X' p = TFALSUM 'U' p;