let r, s be real number ; :: thesis: ( ( ( r in REAL+ & s in REAL+ & ex x', y' being Element of REAL+ st
( r = x' & s = y' & x' <=' y' ) ) or ( r in [:{0 },REAL+ :] & s in [:{0 },REAL+ :] & ex x', y' being Element of REAL+ st
( r = [0 ,x'] & s = [0 ,y'] & y' <=' x' ) ) or ( s in REAL+ & r in [:{0 },REAL+ :] ) ) implies r <= s )
assume A1: ( ( r in REAL+ & s in REAL+ & ex x', y' being Element of REAL+ st
( r = x' & s = y' & x' <=' y' ) ) or ( r in [:{0 },REAL+ :] & s in [:{0 },REAL+ :] & ex x', y' being Element of REAL+ st
( r = [0 ,x'] & s = [0 ,y'] & y' <=' x' ) ) 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 = K121() or s = K120() )
hence ( ( s in REAL+ & r in [:{0 },REAL+ :] ) or r = K121() or s = K120() ) by A1; :: thesis: verum
end;
end;