:: deftheorem defines is_succ2_of MODELC_3:def 8 :
for v being LTL-formula
for N1, N2 being LTLnode over v holds
( N2 is_succ2_of N1 iff ex H being LTL-formula st
( H in the LTLnew of N1 & ( H is disjunctive or H is Until or H is Release ) & N2 = SuccNode2 (H,N1) ) );