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;

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;

end;

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

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;hence x = y by A1, A4, XXREAL_0:def 5; :: thesis: verum

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;hence x = y by A2, A5, XXREAL_0:def 5; :: thesis: verum

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;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