let a, b be R_eal; :: thesis: ( not a <= b or ( a = -infty & b = -infty ) or ( a = -infty & b in REAL ) or ( a = -infty & b = +infty ) or ( a in REAL & b in REAL ) or ( a in REAL & b = +infty ) or ( a = +infty & b = +infty ) )
assume A1: a <= b ; :: thesis: ( ( a = -infty & b = -infty ) or ( a = -infty & b in REAL ) or ( a = -infty & b = +infty ) or ( a in REAL & b in REAL ) or ( a in REAL & b = +infty ) or ( a = +infty & b = +infty ) )
( ( a in REAL or a in {-infty ,+infty } ) & ( b in REAL or b in {-infty ,+infty } ) ) by XBOOLE_0:def 3, XXREAL_0:def 4;
then ( ( a in REAL or a = -infty or a = +infty ) & ( b in REAL or b = -infty or b = +infty ) ) by TARSKI:def 2;
hence ( ( a = -infty & b = -infty ) or ( a = -infty & b in REAL ) or ( a = -infty & b = +infty ) or ( a in REAL & b in REAL ) or ( a in REAL & b = +infty ) or ( a = +infty & b = +infty ) ) by A1, XXREAL_0:9, XXREAL_0:12; :: thesis: verum