let F, G, H be LTL-formula; :: thesis: ( F is_subformula_of G & G is_subformula_of H implies F is_subformula_of H )
assume that
A1: F is_subformula_of G and
A2: G is_subformula_of H ; :: thesis: F is_subformula_of H

now :: thesis: ( F <> G implies F is_subformula_of H )

assume F <> G ; :: thesis: F is_subformula_of H
then A3: F is_proper_subformula_of G by A1;

now :: thesis: ( G <> H implies F is_subformula_of H )

assume G <> H ; :: thesis: F is_subformula_of H
then G is_proper_subformula_of H by A2;
then F is_proper_subformula_of H by A3, Th34;
hence F is_subformula_of H ; :: thesis: verum

end;

hence F is_subformula_of H by A1; :: thesis: verum

end;

hence F is_subformula_of H by A2; :: thesis: verum