:: deftheorem defines NEX_rule LTLAXIO1:def 19 :
for p, q being Element of LTLB_WFF holds
( p NEX_rule q iff q = 'X' p );