theorem Th4: :: ARYTM_0:4

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