theorem Th3: :: ARYTM_0:3

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