let v be LTL-formula; :: thesis: for N being strict LTLnode of 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
let N be strict LTLnode of v; :: thesis: for U being Choice_Function of BOOL (Subformulae v) st not N is elementary holds
chosen_formula (U,N) in the LTLnew of N
let U be Choice_Function of BOOL (Subformulae v); :: thesis: ( not N is elementary implies chosen_formula (U,N) in the LTLnew of N )
set x = the LTLnew of N;
set X = BOOL (Subformulae v);
assume A1: not N is elementary ; :: thesis: chosen_formula (U,N) in the LTLnew of N
then ( not {} in BOOL (Subformulae v) & the LTLnew of N in BOOL (Subformulae v) ) by Th56, ORDERS_1:1;
then U . the LTLnew of N in the LTLnew of N by ORDERS_1:def 1;
hence chosen_formula (U,N) in the LTLnew of N by A1, Def34; :: thesis: verum