theorem Th69: :: ZF_LANG:69

for F, H being ZF-formula st F is_proper_subformula_of 'not' H holds
F is_subformula_of H