let R1, R2 be Relation of the carrier of W; :: thesis: ( ( for x, y being Element of W holds
( [x,y] in R1 iff ( x <= y or y <= x ) ) ) & ( for x, y being Element of W holds
( [x,y] in R2 iff ( x <= y or y <= x ) ) ) implies R1 = R2 )
assume that
A1: for x, y being Element of W holds
( [x,y] in R1 iff ( x <= y or y <= x ) ) and
A2: for x, y being Element of W holds
( [x,y] in R2 iff ( x <= y or y <= x ) ) ; :: thesis: R1 = R2
A3: R1 c= R2

proof

let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in R1 or [x,y] in R2 )
assume A4: [x,y] in R1 ; :: thesis: [x,y] in R2
then reconsider x1 = x, y1 = y as Element of W by ZFMISC_1:87;
( x1 <= y1 or y1 <= x1 ) by A1, A4;
hence [x,y] in R2 by A2; :: thesis: verum

end;

R2 c= R1

proof

let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in R2 or [x,y] in R1 )
assume A4: [x,y] in R2 ; :: thesis: [x,y] in R1
then ( x in the carrier of W & y in the carrier of W ) by ZFMISC_1:87;
then reconsider x1 = x, y1 = y as Element of W ;
( x1 <= y1 or y1 <= x1 ) by A2, A4;
hence [x,y] in R1 by A1; :: thesis: verum

end;

hence R1 = R2 by XBOOLE_0:def 10, A3; :: thesis: verum