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 ( x in RAT+ & y in RAT+ ) ; :: thesis: x = y

then reconsider x9 = x, y9 = y as Element of RAT+ ;
( x9 <=' y9 & y9 <=' x9 ) by A1, A2, Lm14;
hence x = y by ARYTM_3:66; :: thesis: verum

end;

suppose A3: ( x in RAT+ & not y in RAT+ ) ; :: thesis: x = y

x in y by A1, A3, Def5;
hence x = y by A2, A3, Def5; :: thesis: verum

end;

suppose A4: ( not x in RAT+ & y in RAT+ ) ; :: thesis: x = y

y in x by A2, A4, Def5;
hence x = y by A1, A4, Def5; :: thesis: verum

end;

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

then ( x c= y & y c= x ) by A1, A2, Def5;
hence x = y ; :: thesis: verum

end;

end;