theorem Th71: :: ZF_LANG:71

for x being Variable
for F, H being ZF-formula st F is_proper_subformula_of All (x,H) holds
F is_subformula_of H