let x9, y9 be Element of RAT+ ; :: thesis: for x, y being Element of REAL+ st x = x9 & y = y9 holds
( x <=' y iff x9 <=' y9 )
let x, y be Element of REAL+ ; :: thesis: ( x = x9 & y = y9 implies ( x <=' y iff x9 <=' y9 ) )
assume A1: ( x = x9 & y = y9 ) ; :: thesis: ( x <=' y iff x9 <=' y9 )

hereby :: thesis: ( x9 <=' y9 implies x <=' y )

assume x <=' y ; :: thesis: x9 <=' y9
then ex x9, y9 being Element of RAT+ st
( x = x9 & y = y9 & x9 <=' y9 ) by A1, Def5;
hence x9 <=' y9 by A1; :: thesis: verum

end;

thus ( x9 <=' y9 implies x <=' y ) by A1, Def5; :: thesis: verum