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 ) )
( a in REAL or a in {-infty,+infty} ) by XBOOLE_0:def 3, XXREAL_0:def 4;
then A1: ( a in REAL or a = -infty or a = +infty ) by TARSKI:def 2;
( b in REAL or b in {-infty,+infty} ) by XBOOLE_0:def 3, XXREAL_0:def 4;
then A2: ( b in REAL or b = -infty or b = +infty ) by TARSKI:def 2;
assume 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 ) )
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, A2, XXREAL_0:9, XXREAL_0:12; :: thesis: verum