let F, G be ZF-formula; :: thesis: ( F is_subformula_of G implies len F <= len G )
assume F is_subformula_of G ; :: thesis: len F <= len G
then ( F is_proper_subformula_of G or F = G ) by ZF_LANG:def 41;
hence len F <= len G by ZF_LANG:62; :: thesis: verum