:: deftheorem Def4 defines |= ZF_MODEL:def 4 :
for D being non empty set
for f being Function of VAR,D
for H being ZF-formula holds
( D,f |= H iff f in St (H,D) );