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

( 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