set R = LatOrder W;
for x, y being object st [x,y] in LatOrder W & [y,x] in LatOrder W holds
x = y

proof

let x, y be object ; :: thesis: ( [x,y] in LatOrder W & [y,x] in LatOrder W implies x = y )
assume A1: ( [x,y] in LatOrder W & [y,x] in LatOrder W ) ; :: thesis: x = y
then reconsider x1 = x, y1 = y as Element of W by ZFMISC_1:87;
( x1 [= y1 & y1 [= x1 ) by A1, Idem2;
hence x = y by LATTICES:8; :: thesis: verum

end;

hence LatOrder W is antisymmetric by PREFER_1:31; :: thesis: verum