:: deftheorem defines is_next_of MODELC_3:def 20 :
for v being LTL-formula
for N1, N2 being strict LTLnode over v holds
( N2 is_next_of N1 iff ( N1 is elementary & N2 is elementary & ex L being FinSequence st
( 1 <= len L & L is_Finseq_for v & L . 1 = 'X' N1 & L . (len L) = N2 ) ) );