theorem Th25: :: MODELC_3:25

for v being LTL-formula
for N1, N2 being strict LTLnode over v st N2 is_succ_of N1 holds
( the LTLold of N1 c= the LTLold of N2 & the LTLnext of N1 c= the LTLnext of N2 )