theorem Th58: :: MODELC_3:58

for v being LTL-formula
for N being strict LTLnode over v
for U being Choice_Function of (BOOL (Subformulae v)) st not N is elementary holds
chosen_formula (U,N) in the LTLnew of N