for y being set st [{},y] in REAL holds
y <> {}