theorem Th78: :: ZF_LANG:78

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