theorem :: ARYTM_1:18

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