let x, y be Element of REAL+ ; :: thesis: ( x <=' y & y <=' x implies x = y )
assume that
A1: x <=' y and
A2: y <=' x ; :: thesis: x = y

per cases ( ( x in RAT+ & y in RAT+ ) or ( x in RAT+ & not y in RAT+ ) or ( not x in RAT+ & y in RAT+ ) or ( not x in RAT+ & not y in RAT+ ) ) ;

suppose that A3: x in RAT+ and
A4: y in RAT+ ; :: thesis: x = y

reconsider x' = x, y' = y as Element of RAT+ by A3, A4;
( x' <=' y' & y' <=' x' ) by A1, A2, Lm14;
hence x = y by ARYTM_3:73; :: thesis: verum

end;

suppose that A5: x in RAT+ and
A6: not y in RAT+ ; :: thesis: x = y

( x in y & not x in y ) by A1, A2, A5, A6, Def5;
hence x = y ; :: thesis: verum

end;

suppose that A7: not x in RAT+ and
A8: y in RAT+ ; :: thesis: x = y

( y in x & not y in x ) by A1, A2, A7, A8, Def5;
hence x = y ; :: thesis: verum

end;

suppose that A9: not x in RAT+ and
A10: not y in RAT+ ; :: thesis: x = y

( x c= y & y c= x ) by A1, A2, A9, A10, Def5;
hence x = y by XBOOLE_0:def 10; :: thesis: verum

end;

end;