let v be LTL-formula; :: thesis: for N being strict LTLnode over 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 over 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:89;
hence chosen_formula (U,N) in the LTLnew of N by A1, Def34; :: thesis: verum