theorem :: SUPINF_2:1

for x, y being ExtReal
for a, b being Real st x = a & y = b holds
x + y = a + b by XXREAL_3:def 2;