theorem :: XXREAL_3:28

for y, z being ExtReal st 0 <= y & y < +infty holds
z = (z + y) - y