theorem :: ZF_LANG:72

for F, H being ZF-formula st H is atomic holds
not F is_proper_subformula_of H