theorem Th67: :: ZF_LANG:67

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