let x, y be ext-real number ; :: thesis: ( ( x = +infty & y = +infty ) or ( x = -infty & y = -infty ) or not x - y in REAL or ( x in REAL & y in REAL ) )
assume A1: ( not ( x = +infty & y = +infty ) & not ( x = -infty & y = -infty ) & x - y in REAL ) ; :: thesis: ( x in REAL & y in REAL )
assume A2: ( not x in REAL or not y in REAL ) ; :: thesis: contradiction
( ( x in REAL or x = -infty or x = +infty ) & ( y in REAL or y = -infty or y = +infty ) ) by XXREAL_0:14;
hence contradiction by A1, A2, Th16, Th29; :: thesis: verum