let S be full SubRelStr of L; :: thesis: S is transitive
let x, y, z be Element of S; :: according to YELLOW_0:def 2 :: thesis: ( x <= y & y <= z implies x <= z )
assume A1: ( x <= y & y <= z ) ; :: thesis: x <= z
then ( [x,y] in the InternalRel of S & [y,z] in the InternalRel of S ) by ORDERS_2:def 9;
then A2: ( x in the carrier of S & y in the carrier of S & z in the carrier of S ) by ZFMISC_1:106;
the carrier of S c= the carrier of L by Def13;
then reconsider a = x, b = y, c = z as Element of L by A2;
( a <= b & b <= c ) by A1, Th60;
hence x <= z by A2, Th61, ORDERS_2:26; :: thesis: verum