set R = LatOrder W;
for x being Element of W holds [x,x] in LatOrder W

proof

let x be Element of W; :: thesis: [x,x] in LatOrder W
x [= x ;
hence [x,x] in LatOrder W ; :: thesis: verum

end;

hence LatOrder W is reflexive by LATTAD_1:1; :: thesis: verum