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

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

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

end;

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