for x, y being Element of REAL+ holds x - y in REAL