let x, y be Real; :: 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 x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & x9 <=' y9 ) & ex y99, x99 being Element of REAL+ st
( y = y99 & x = x99 & y99 <=' x99 ) ) 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 x9, y9 being Element of REAL+ such that
A7: ( x = [0,x9] & y = [0,y9] ) and
A8: y9 <=' x9 by A1, A6, XXREAL_0:def 5;
consider y99, x99 being Element of REAL+ such that
A9: ( y = [0,y99] & x = [0,x99] ) and
A10: x99 <=' y99 by A2, A6, XXREAL_0:def 5;
( x9 = x99 & y9 = y99 ) by A7, A9, XTUPLE_0:1;
hence x = y by A8, A9, A10, ARYTM_1:4; :: thesis: verum

end;

end;