for F, H being ZF-formula
for x being Variable st All (x,H) is_subformula_of F holds
H is_proper_subformula_of F