for x, y being Element of REAL+ ex z being Element of REAL+ st
( x + z = y or y + z = x )