let x, y be real number ; :: thesis: ( x <= y & y <= x implies x = y )
assume that
A1: x <= y and
A2: y <= x ; :: thesis: x = y
A3: ( x in REAL & y in REAL ) by XREAL_0:def 1;

per cases ( ( x in REAL+ & y in REAL+ ) or ( x in REAL+ & y in [:{0 },REAL+ :] ) or ( y in REAL+ & x in [:{0 },REAL+ :] ) or ( x in [:{0 },REAL+ :] & y in [:{0 },REAL+ :] ) ) by A3, NUMBERS:def 1, XBOOLE_0:def 3;

suppose ( x in REAL+ & y in REAL+ ) ; :: thesis: x = y

then ( ex x', y' being Element of REAL+ st
( x = x' & y = y' & x' <=' y' ) & ex y'', x'' being Element of REAL+ st
( y = y'' & x = x'' & y'' <=' x'' ) ) by A1, A2, XXREAL_0:def 5;
hence x = y by ARYTM_1:4; :: thesis: verum

end;

suppose A4: ( x in REAL+ & y in [:{0 },REAL+ :] ) ; :: thesis: x = y

then ( ( not x in REAL+ or not y in REAL+ ) & ( not x in [:{0 },REAL+ :] or not y in [:{0 },REAL+ :] ) ) by ARYTM_0:5, XBOOLE_0:3;
hence x = y by A1, A4, XXREAL_0:def 5; :: thesis: verum

end;

suppose A5: ( y in REAL+ & x in [:{0 },REAL+ :] ) ; :: thesis: x = y

then ( ( not x in REAL+ or not y in REAL+ ) & ( not x in [:{0 },REAL+ :] or not y in [:{0 },REAL+ :] ) ) by ARYTM_0:5, XBOOLE_0:3;
hence x = y by A2, A5, XXREAL_0:def 5; :: thesis: verum

end;

suppose A6: ( x in [:{0 },REAL+ :] & y in [:{0 },REAL+ :] ) ; :: thesis: x = y

consider x', y' being Element of REAL+ such that
A7: ( x = [0 ,x'] & y = [0 ,y'] ) and
A8: y' <=' x' by A1, A6, XXREAL_0:def 5;
consider y'', x'' being Element of REAL+ such that
A9: ( y = [0 ,y''] & x = [0 ,x''] ) and
A10: x'' <=' y'' by A2, A6, XXREAL_0:def 5;
( x' = x'' & y' = y'' ) by A7, A9, ZFMISC_1:33;
hence x = y by A8, A9, A10, ARYTM_1:4; :: thesis: verum

end;

end;