for F, G being ZF-formula st F is_subformula_of G holds
len F <= len G by ZF_LANG:def 41, ZF_LANG:62;