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

( 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 5end;

:: according to XXREAL_0:def 5

case
( r in REAL+ & s in REAL+ )
; :: thesis: ex b_{1}, b_{2} being Element of REAL+ st

( r = b_{1} & s = b_{2} & b_{1} <=' b_{2} )

( r = b

hence
ex b_{1}, b_{2} being Element of REAL+ st

( r = b_{1} & s = b_{2} & b_{1} <=' b_{2} )
by A1, ARYTM_0:5, XBOOLE_0:3; :: thesis: verum

end;( r = b

case
( r in [:{0},REAL+:] & s in [:{0},REAL+:] )
; :: thesis: ex b_{1}, b_{2} being Element of REAL+ st

( r = [0,b_{1}] & s = [0,b_{2}] & b_{2} <=' b_{1} )

( r = [0,b

hence
ex b_{1}, b_{2} being Element of REAL+ st

( r = [0,b_{1}] & s = [0,b_{2}] & b_{2} <=' b_{1} )
by A1, ARYTM_0:5, XBOOLE_0:3; :: thesis: verum

end;( r = [0,b