:: deftheorem Def34 defines chosen_formula MODELC_3:def 34 :
for v being LTL-formula
for U being Choice_Function of (BOOL (Subformulae v))
for N being strict LTLnode over v st not N is elementary holds
chosen_formula (U,N) = U . the LTLnew of N;