theorem :: XXREAL_3:24

for x, z being ExtReal st z is real holds
x = (x + z) - z