theorem Th11: :: ARYTM_2:11

for x, y, z being Element of REAL+ st x + y = x + z holds
y = z