theorem Th56: :: MODELC_3:56

for v being LTL-formula
for N being strict LTLnode over v st not N is elementary holds
( the LTLnew of N <> {} & the LTLnew of N in BOOL (Subformulae v) ) by ORDERS_1:2;