theorem :: ARYTM_3:61

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