for G, H being ZF-formula holds
( G is_subformula_of H iff G in Subformulae H ) by ZF_LANG:78, ZF_LANG:def 42;