theorem Th15: :: XXREAL_3:15

for x being ExtReal holds x - 0 = x