let x be ExtReal; :: 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 ;
x - 0 = a - 0
.= x ;
hence x - 0 = x ; :: thesis: verum

end;

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

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

end;

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

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

end;

end;