ex F being LTL-formula st
( H = F & F is_subformula_of v ) by A1, MODELC_2:def 24;
then Subformulae H c= Subformulae v by MODELC_2:46;
hence LTLNew1 H is Subset of (Subformulae v) by XBOOLE_1:1; :: thesis: verum