theorem :: ZF_LANG:73

for H being ZF-formula st H is negative holds
the_argument_of H is_proper_subformula_of H