let G, H be ZF-formula; :: thesis: ( G in Subformulae H implies G is_subformula_of H )
assume G in Subformulae H ; :: thesis: G is_subformula_of H
then ex F being ZF-formula st
( F = G & F is_subformula_of H ) by Def42;
hence G is_subformula_of H ; :: thesis: verum