let H, v be LTL-formula; :: thesis: ( H in Subformulae v implies len (LTLNew1 (H,v)) <= (len H) - 1 )
set New = LTLNew1 (H,v);
set Left = {(the_left_argument_of H)};
set Right = {(the_right_argument_of H)};
assume A1: H in Subformulae v ; :: thesis: len (LTLNew1 (H,v)) <= (len H) - 1
then A2: LTLNew1 (H,v) = LTLNew1 H by Def27;
ex F being LTL-formula st
( H = F & F is_subformula_of v ) by A1, MODELC_2:def 24;
then A3: Subformulae H c= Subformulae v by MODELC_2:46;

now :: thesis: len (LTLNew1 (H,v)) <= (len H) - 1

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 A4: H is conjunctive ; :: thesis: len (LTLNew1 (H,v)) <= (len H) - 1

then {(the_right_argument_of H)} is Subset of (Subformulae H) by Lm12;
then reconsider Right = {(the_right_argument_of H)} as Subset of (Subformulae v) by A3, XBOOLE_1:1;
{(the_left_argument_of H)} is Subset of (Subformulae H) by A4, Lm12;
then reconsider Left = {(the_left_argument_of H)} as Subset of (Subformulae v) by A3, XBOOLE_1:1;
LTLNew1 (H,v) = {(the_left_argument_of H),(the_right_argument_of H)} by A2, A4, Def1;
then LTLNew1 (H,v) = Left \/ Right by ENUMSET1:1;
then A5: len (LTLNew1 (H,v)) <= (len Left) + (len Right) by Th18;
A6: len H = (1 + (len (the_left_argument_of H))) + (len (the_right_argument_of H)) by A4, MODELC_2:11;
( len Left = len (the_left_argument_of H) & len Right = len (the_right_argument_of H) ) by Th14;
hence len (LTLNew1 (H,v)) <= (len H) - 1 by A6, A5; :: thesis: verum

end;

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

then LTLNew1 (H,v) = {(the_left_argument_of H)} by A2, Def1;
then len (LTLNew1 (H,v)) = len (the_left_argument_of H) by Th14;
then A8: (len (LTLNew1 (H,v))) + 0 <= (len (the_left_argument_of H)) + (len (the_right_argument_of H)) by XREAL_1:7;
len H = (1 + (len (the_left_argument_of H))) + (len (the_right_argument_of H)) by A7, MODELC_2:11;
hence len (LTLNew1 (H,v)) <= (len H) - 1 by A8; :: thesis: verum

end;

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

1 <= len H by MODELC_2:3;
then A10: 1 - 1 <= (len H) - 1 by XREAL_1:9;
LTLNew1 (H,v) = {} v by A2, A9, Def1;
hence len (LTLNew1 (H,v)) <= (len H) - 1 by A10, Th13; :: thesis: verum

end;

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

then LTLNew1 (H,v) = {(the_right_argument_of H)} by A2, Def1;
then len (LTLNew1 (H,v)) = len (the_right_argument_of H) by Th14;
then A12: (len (LTLNew1 (H,v))) + 0 <= (len (the_left_argument_of H)) + (len (the_right_argument_of H)) by XREAL_1:7;
len H = (1 + (len (the_left_argument_of H))) + (len (the_right_argument_of H)) by A11, MODELC_2:11;
hence len (LTLNew1 (H,v)) <= (len H) - 1 by A12; :: thesis: verum

end;

suppose A13: ( 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 A14: 1 - 1 <= (len H) - 1 by XREAL_1:9;
LTLNew1 (H,v) = {} v by A2, A13, Def1;
hence len (LTLNew1 (H,v)) <= (len H) - 1 by A14, Th13; :: thesis: verum

end;

end;

end;

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