theorem Th6: :: ARYTM_0:6

for x, y being Element of REAL+ st x - y = {} holds
x = y