let r, s be Real; :: 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;