let r, s be real number ; :: thesis: ( ( ( r in REAL+ & s in REAL+ & ex x9, y9 being Element of REAL+ st
( r = x9 & s = y9 & x9 <=' y9 ) ) or ( r in [:{0 },REAL+ :] & s in [:{0 },REAL+ :] & ex x9, y9 being Element of REAL+ st
( r = [0 ,x9] & s = [0 ,y9] & y9 <=' x9 ) ) or ( s in REAL+ & r in [:{0 },REAL+ :] ) ) implies r <= s )
assume A1: ( ( r in REAL+ & s in REAL+ & ex x9, y9 being Element of REAL+ st
( r = x9 & s = y9 & x9 <=' y9 ) ) or ( r in [:{0 },REAL+ :] & s in [:{0 },REAL+ :] & ex x9, y9 being Element of REAL+ st
( r = [0 ,x9] & s = [0 ,y9] & y9 <=' x9 ) ) or ( s in REAL+ & r in [:{0 },REAL+ :] ) ) ; :: thesis: r <= s
per cases ( ( r in REAL+ & s in REAL+ ) or ( r in [:{0 },REAL+ :] & s in [:{0 },REAL+ :] ) or ( ( not r in REAL+ or not s in REAL+ ) & ( not r in [:{0 },REAL+ :] or not s in [:{0 },REAL+ :] ) ) ) ;
:: according to XXREAL_0:def 5
case ( r in REAL+ & s in REAL+ ) ; :: thesis: ex b1, b2 being Element of REAL+ st
( r = b1 & s = b2 & b1 <=' b2 )
hence ex b1, b2 being Element of REAL+ st
( r = b1 & s = b2 & b1 <=' b2 ) by A1, ARYTM_0:5, XBOOLE_0:3; :: thesis: verum
end;
case ( r in [:{0 },REAL+ :] & s in [:{0 },REAL+ :] ) ; :: thesis: ex b1, b2 being Element of REAL+ st
( r = [0 ,b1] & s = [0 ,b2] & b2 <=' b1 )
hence ex b1, b2 being Element of REAL+ st
( r = [0 ,b1] & s = [0 ,b2] & b2 <=' b1 ) by A1, ARYTM_0:5, XBOOLE_0:3; :: thesis: verum
end;
case ( ( not r in REAL+ or not s in REAL+ ) & ( not r in [:{0 },REAL+ :] or not s in [:{0 },REAL+ :] ) ) ; :: thesis: ( ( s in REAL+ & r in [:{0 },REAL+ :] ) or r = -infty or s = +infty )
hence ( ( s in REAL+ & r in [:{0 },REAL+ :] ) or r = -infty or s = +infty ) by A1; :: thesis: verum
end;
end;