let x, s be R_eal; :: thesis: ( not x - s = +infty or x = +infty or s = -infty )
assume A1: x - s = +infty ; :: thesis: ( x = +infty or s = -infty )
assume A2: ( not x = +infty & not s = -infty ) ; :: thesis: contradiction
( ( x in REAL or x in {-infty ,+infty } ) & ( s in REAL or s in {-infty ,+infty } ) ) by XBOOLE_0:def 3;
then A3: ( ( x in REAL & s in REAL ) or ( x in REAL & s = +infty ) or ( x = -infty & s in REAL ) or ( x = -infty & s = +infty ) ) by A2, TARSKI:def 2;
( not x in REAL or not s in REAL )

proof

assume ( x in REAL & s in REAL ) ; :: thesis: contradiction
then reconsider a = x, b = s as Real ;
x - s = a - b by Th5;
hence contradiction by A1; :: thesis: verum

end;

hence contradiction by A1, A3, Th6, Th7; :: thesis: verum