set x = the LTLnew of N;
set a = U . the LTLnew of N;
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;
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