let H, v be LTL-formula; :: thesis: ( H in Subformulae v implies len (LTLNew1 H,v) <= (len H) - 1 )
assume A1: H in Subformulae v ; :: thesis: len (LTLNew1 H,v) <= (len H) - 1
set New = LTLNew1 H,v;
A01: LTLNew1 H,v = LTLNew1 H by A1, defLTLNew101;
set Left = {(the_left_argument_of H)};
set Right = {(the_right_argument_of H)};
consider F being LTL-formula such that
A2: H = F and
A3: F is_subformula_of v by A1, MODELC_2:def 24;
A4: Subformulae H c= Subformulae v by A2, A3, MODELC_2:46;

now

per cases ( H is conjunctive or H is disjunctive or H is Until or H is next or H is Release or ( not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release ) ) ;

suppose A5: H is conjunctive ; :: thesis: len (LTLNew1 H,v) <= (len H) - 1

{(the_left_argument_of H)} is Subset of (Subformulae H) by A5, Lem108;
then reconsider Left = {(the_left_argument_of H)} as Subset of (Subformulae v) by A4, XBOOLE_1:1;
{(the_right_argument_of H)} is Subset of (Subformulae H) by A5, Lem108;
then reconsider Right = {(the_right_argument_of H)} as Subset of (Subformulae v) by A4, XBOOLE_1:1;
B1: len Left = len (the_left_argument_of H) by Thlen11;
B2: len Right = len (the_right_argument_of H) by Thlen11;
B3: len H = (1 + (len (the_left_argument_of H))) + (len (the_right_argument_of H)) by A5, MODELC_2:11;
LTLNew1 H,v = {(the_left_argument_of H),(the_right_argument_of H)} by A01, A5, Def203;
then LTLNew1 H,v = Left \/ Right by ENUMSET1:41;
then len (LTLNew1 H,v) <= (len Left) + (len Right) by Thlen13;
hence len (LTLNew1 H,v) <= (len H) - 1 by B1, B2, B3; :: thesis: verum

end;

suppose A6: ( H is disjunctive or H is Until ) ; :: thesis: len (LTLNew1 H,v) <= (len H) - 1

B2: len H = (1 + (len (the_left_argument_of H))) + (len (the_right_argument_of H)) by A6, MODELC_2:11;
LTLNew1 H,v = {(the_left_argument_of H)} by A01, A6, Def203;
then len (LTLNew1 H,v) = len (the_left_argument_of H) by Thlen11;
then (len (LTLNew1 H,v)) + 0 <= (len (the_left_argument_of H)) + (len (the_right_argument_of H)) by XREAL_1:9;
hence len (LTLNew1 H,v) <= (len H) - 1 by B2; :: thesis: verum

end;

suppose A7: H is next ; :: thesis: len (LTLNew1 H,v) <= (len H) - 1

1 <= len H by MODELC_2:3;
then B1: 1 - 1 <= (len H) - 1 by XREAL_1:11;
LTLNew1 H,v = {} v by A01, A7, Def203;
hence len (LTLNew1 H,v) <= (len H) - 1 by B1, Thlen10; :: thesis: verum

end;

suppose A8: H is Release ; :: thesis: len (LTLNew1 H,v) <= (len H) - 1

B2: len H = (1 + (len (the_left_argument_of H))) + (len (the_right_argument_of H)) by A8, MODELC_2:11;
LTLNew1 H,v = {(the_right_argument_of H)} by A01, A8, Def203;
then len (LTLNew1 H,v) = len (the_right_argument_of H) by Thlen11;
then (len (LTLNew1 H,v)) + 0 <= (len (the_left_argument_of H)) + (len (the_right_argument_of H)) by XREAL_1:9;
hence len (LTLNew1 H,v) <= (len H) - 1 by B2; :: thesis: verum

end;

suppose A9: ( not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release ) ; :: thesis: len (LTLNew1 H,v) <= (len H) - 1

1 <= len H by MODELC_2:3;
then B1: 1 - 1 <= (len H) - 1 by XREAL_1:11;
LTLNew1 H,v = {} v by A01, A9, Def203;
hence len (LTLNew1 H,v) <= (len H) - 1 by Thlen10, B1; :: thesis: verum

end;

end;

end;

hence len (LTLNew1 H,v) <= (len H) - 1 ; :: thesis: verum