set x = the LTLnew of N;
set a = U . the LTLnew of N;
not {} in BOOL (Subformulae v) by ORDERS_1:1;
then A2: U is Function of (BOOL (Subformulae v)),(union (BOOL (Subformulae v))) by ORDERS_1:90;
the LTLnew of N in BOOL (Subformulae v) by A1, Th56;
then U . the LTLnew of N in union (BOOL (Subformulae v)) by FUNCT_2:5, A2;
then U . the LTLnew of N in Subformulae v by Th55;
then ex F being LTL-formula st
( F = U . the LTLnew of N & F is_subformula_of v ) by MODELC_2:def 24;
hence U . the LTLnew of N is LTL-formula ; :: thesis: verum