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