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

proof

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

end;

hence LatOrder L is reflexive by Ble1; :: thesis: verum