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

proof

let x, y, z be object ; :: thesis: ( [x,y] in LatOrder L & [y,z] in LatOrder L implies [x,z] in LatOrder L )
assume A1: ( [x,y] in LatOrder L & [y,z] in LatOrder L ) ; :: thesis: [x,z] in LatOrder L
then consider x1, y1 being object such that
A2: ( [x,y] = [x1,y1] & x1 in the carrier of L & y1 in the carrier of L ) by RELSET_1:2;
consider y2, z2 being object such that
A3: ( [y,z] = [y2,z2] & y2 in the carrier of L & z2 in the carrier of L ) by A1, RELSET_1:2;
reconsider xx = x, yy = y, zz = z as Element of L by A2, A3, XTUPLE_0:1;
( xx [= yy & yy [= zz ) by A1, OrdLat;
then xx [= zz by TransLat;
hence [x,z] in LatOrder L ; :: thesis: verum

end;

hence LatOrder L is transitive by RELAT_2:31; :: thesis: verum