let G, H be LTL-formula; :: thesis: ( G in Subformulae H iff G is_subformula_of H )
( G in Subformulae H implies G is_subformula_of H )

proof

assume G in Subformulae H ; :: thesis: G is_subformula_of H
then ex F being LTL-formula st
( F = G & F is_subformula_of H ) by Def24;
hence G is_subformula_of H ; :: thesis: verum

end;

hence ( G in Subformulae H iff G is_subformula_of H ) by Def24; :: thesis: verum