theorem :: XXREAL_3:105

for x being ExtReal holds (x / 2) + (x / 2) = x