let x be ext-real number ; :: thesis: x - 0 = x

per cases ( x in REAL or x = -infty or x = +infty ) by XXREAL_0:14;

suppose x in REAL ; :: thesis: x - 0 = x

then reconsider a = x as real number ;
x - 0 = a - 0
.= x ;
hence x - 0 = x ; :: thesis: verum

end;

suppose x = -infty ; :: thesis: x - 0 = x

hence x - 0 = x by Th29; :: thesis: verum

end;

suppose x = +infty ; :: thesis: x - 0 = x

hence x - 0 = x by Th16; :: thesis: verum

end;

end;