:: deftheorem Def28 defines LTLNew2 MODELC_3:def 28 :
for v, H being LTL-formula st H in Subformulae v holds
LTLNew2 (H,v) = LTLNew2 H;