let R be non empty real RelStr ; :: thesis: for x, y being Element of R holds
( x <= y iff x <<= y )
let x, y be Element of R; :: thesis: ( x <= y iff x <<= y )
( [x,y] in the InternalRel of R iff x <= y ) by Def1;
hence ( x <= y iff x <<= y ) by ORDERS_2:def 5; :: thesis: verum