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 ) or ( y in REAL+ & x in ) or ( x in & y in ) ) by ;
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 ;
hence x = y by ARYTM_1:4; :: thesis: verum
end;
suppose A4: ( x in REAL+ & y in ) ; :: thesis: x = y
then ( ( not x in REAL+ or not y in REAL+ ) & ( not x in or not y in ) ) by ;
hence x = y by ; :: thesis: verum
end;
suppose A5: ( y in REAL+ & x in ) ; :: thesis: x = y
then ( ( not x in REAL+ or not y in REAL+ ) & ( not x in or not y in ) ) by ;
hence x = y by ; :: thesis: verum
end;
suppose A6: ( x in & y in ) ; :: thesis: x = y
consider x9, y9 being Element of REAL+ such that
A7: ( x = [0,x9] & y = [0,y9] ) and
A8: y9 <=' x9 by ;
consider y99, x99 being Element of REAL+ such that
A9: ( y = [0,y99] & x = [0,x99] ) and
A10: x99 <=' y99 by ;
( x9 = x99 & y9 = y99 ) by ;
hence x = y by ; :: thesis: verum
end;
end;