theorem Th94: :: XXREAL_3:94

for x being ExtReal holds 2 * x = x + x