theorem :: ZF_MODEL:9

for H being ZF-formula
for E being non empty set st H is negative holds
for f being Function of VAR,E holds
( not f in St ((the_argument_of H),E) iff f in St (H,E) )