for E being non empty set
for f being Function of VAR,E
for H, H9 being ZF-formula holds
( E,f |= H <=> H9 iff ( E,f |= H iff E,f |= H9 ) )