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 & s in & ex x9, y9 being Element of REAL+ st
( r = [0,x9] & s = [0,y9] & y9 <=' x9 ) ) or ( s in REAL+ & r in ) ) 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 & s in & ex x9, y9 being Element of REAL+ st
( r = [0,x9] & s = [0,y9] & y9 <=' x9 ) ) or ( s in REAL+ & r in ) ) ; :: thesis: r <= s
per cases ( ( r in REAL+ & s in REAL+ ) or ( r in & s in ) or ( ( not r in REAL+ or not s in REAL+ ) & ( not r in or not s in ) ) ) ;
:: 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 ; :: thesis: verum
end;
case ( r in & s in ) ; :: 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 ; :: thesis: verum
end;
case ( ( not r in REAL+ or not s in REAL+ ) & ( not r in or not s in ) ) ; :: thesis: ( ( s in REAL+ & r in ) or r = -infty or s = +infty )
hence ( ( s in REAL+ & r in ) or r = -infty or s = +infty ) by A1; :: thesis: verum
end;
end;