let x, y, z be object ; :: thesis: ( [x,y] in ThetaOrder L & [y,z] in ThetaOrder L implies [x,z] in ThetaOrder L )
assume A1: ( [x,y] in ThetaOrder L & [y,z] in ThetaOrder L ) ; :: thesis: [x,z] in ThetaOrder 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 "/\" zz = xx "/\" (yy "/\" zz) by A1, ThetaOrdLat
.= (xx "/\" yy) "/\" zz by LATTICES:def 7
.= yy "/\" zz by A1, ThetaOrdLat
.= zz by A1, ThetaOrdLat ;
hence [x,z] in ThetaOrder L ; :: thesis: verum