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