let G, H be LTL-formula; :: thesis: ( G is_subformula_of H & H is_subformula_of G implies G = H )
assume A1: ( G is_subformula_of H & H is_subformula_of G ) ; :: thesis: G = H
assume G <> H ; :: thesis: contradiction
then ( G is_proper_subformula_of H & H is_proper_subformula_of G ) by A1, Def102;
then ( len G < len H & len H < len G ) by Th118;
hence contradiction ; :: thesis: verum