:: deftheorem defines is_succ1_of MODELC_3:def 7 :
for v being LTL-formula
for N1, N2 being LTLnode over v holds
( N2 is_succ1_of N1 iff ex H being LTL-formula st
( H in the LTLnew of N1 & N2 = SuccNode1 (H,N1) ) );