let F, H be LTL-formula; :: thesis: ( H is_immediate_constituent_of F implies len H < len F )
assume A1: H is_immediate_constituent_of F ; :: thesis: len H < len F

per cases ( F is negative or F is next or F is conjunctive or F is disjunctive or F is Until or F is Release ) by A1;

suppose A2: ( F is negative or F is next ) ; :: thesis: len H < len F

then H = the_argument_of F by A1, Th20, Th21;
hence len H < len F by A2, Th10; :: thesis: verum

end;

suppose A3: ( F is conjunctive or F is disjunctive or F is Until or F is Release ) ; :: thesis: len H < len F

then ( H = the_left_argument_of F or H = the_right_argument_of F ) by A1, Th22, Th23, Th24, Th25;
hence len H < len F by A3, Th11; :: thesis: verum

end;

end;