theorem :: ARYTM_2:3

for y being object holds not [{},y] in REAL+