:: deftheorem defines next MODELC_2:def 15 :
for H being LTL-formula holds
( H is next iff ex H1 being LTL-formula st H = 'X' H1 );