theorem Th4: :: ZF_MODEL:4

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