let v be LTL-formula; :: thesis: for N being strict LTLnode of v st not N is elementary holds
( the LTLnew of N <> {} & the LTLnew of N in BOOL (Subformulae v) )
let N be strict LTLnode of v; :: thesis: ( not N is elementary implies ( the LTLnew of N <> {} & the LTLnew of N in BOOL (Subformulae v) ) )
set x = the LTLnew of N;
assume not N is elementary ; :: thesis: ( the LTLnew of N <> {} & the LTLnew of N in BOOL (Subformulae v) )
then the LTLnew of N <> {} by Defelementary;
hence ( the LTLnew of N <> {} & the LTLnew of N in BOOL (Subformulae v) ) by ORDERS_1:5; :: thesis: verum