let x be R_eal; :: thesis: x - 0. = x
A1: ( x in REAL or x in {-infty ,+infty } ) by XBOOLE_0:def 3, XXREAL_0:def 4;

per cases ( x in REAL or x = -infty or x = +infty ) by A1, TARSKI:def 2;

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

then reconsider a = x as Real ;
x - 0. = a - 0 by SUPINF_2:5
.= x ;
hence x - 0. = x ; :: thesis: verum

end;

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

hence x - 0. = x by SUPINF_2:7; :: thesis: verum

end;

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

hence x - 0. = x by SUPINF_2:6; :: thesis: verum

end;

end;