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