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 )

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

( 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 <= yassume
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;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

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