theorem Th68: :: ZF_LANG:68

for x, y being Variable
for F being ZF-formula holds not F is_proper_subformula_of x 'in' y