let R be non empty real RelStr ; :: thesis: for x, y being Element of holds
( x <= y iff x <<= y )
let x, y be Element of ; :: 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 9; :: thesis: verum