theorem Th4: :: ARYTM_1:4

for x, y being Element of REAL+ st x <=' y & y <=' x holds
x = y