theorem :: ZF_LANG1:46

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