:: deftheorem defines is_succ_of MODELC_3:def 9 :
for v being LTL-formula
for N1, N2 being LTLnode over v holds
( N2 is_succ_of N1 iff ( N2 is_succ1_of N1 or N2 is_succ2_of N1 ) );