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