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 )
assume A1: not N is elementary ; :: thesis: chosen_formula U,N in the LTLnew of N
set x = the LTLnew of N;
set X = BOOL (Subformulae v);
( not BOOL (Subformulae v) is empty & not {} in BOOL (Subformulae v) & the LTLnew of N in BOOL (Subformulae v) ) by A1, ThBOOL02, ORDERS_1:4;
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 Defchosenformula, A1; :: thesis: verum