:: deftheorem Def27 defines LTLNew1 MODELC_3:def 27 :
for v, H being LTL-formula st H in Subformulae v holds
LTLNew1 (H,v) = LTLNew1 H;