let x, y be ExtReal; :: thesis: ( not x - y = +infty or x = +infty or y = -infty )
assume A1: x - y = +infty ; :: thesis: ( x = +infty or y = -infty )
assume ( not x = +infty & not y = -infty ) ; :: thesis: contradiction
then ( ( x in REAL & y in REAL ) or ( x in REAL & y = +infty ) or ( x = -infty & y in REAL ) or ( x = -infty & y = +infty ) ) by XXREAL_0:14;
hence contradiction by A1, Th13, Th14; :: thesis: verum