theorem Th4: :: XXREAL_3:4

for x being ExtReal holds x + 0 = x