let DP be non empty discrete RelStr ; :: thesis: for x, y being Element of DP holds
( x <= y iff x = y )
let x, y be Element of DP; :: thesis: ( x <= y iff x = y )

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

assume x <= y ; :: thesis: x = y
then [x,y] in the InternalRel of DP by ORDERS_2:def 5;
then [x,y] in id the carrier of DP by Def1;
hence x = y by RELAT_1:def 10; :: thesis: verum

end;

assume x = y ; :: thesis: x <= y
then [x,y] in id the carrier of DP by RELAT_1:def 10;
then [x,y] in the InternalRel of DP by Def1;
hence x <= y by ORDERS_2:def 5; :: thesis: verum