theorem Th59: :: ZF_LANG:59

for H being ZF-formula holds H is_subformula_of H