set x = the LTLnew of N;
set a = U . the LTLnew of N;
the LTLnew of N in BOOL (Subformulae v) by A1, ThBOOL02;
then U . the LTLnew of N in union (BOOL (Subformulae v)) by FUNCT_2:7;
then U . the LTLnew of N in Subformulae v by ThBOOL01;
then consider F being LTL-formula such that
B1: ( F = U . the LTLnew of N & F is_subformula_of v ) by MODELC_2:def 24;
thus U . the LTLnew of N is LTL-formula by B1; :: thesis: verum