for G, H being ZF-formula st G in Subformulae H holds
G is_subformula_of H