let R be non empty asymmetric 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 )

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

assume Z0: x <= y ; :: thesis: x < y
then x <> y ;
hence x < y by Z0, ORDERS_2:def 6; :: thesis: verum

end;

assume x < y ; :: thesis: x <= y
hence x <= y by ORDERS_2:def 6; :: thesis: verum