theorem :: XXREAL_3:12

for r being Real
for f, g being ExtReal st r - f = r - g holds
f = g