theorem Th94: :: XXREAL_3:94
for x being ExtReal holds 2 * x = x + x