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 that
A1: x <= y and
A2: y <= z ; :: thesis: x <= z
A3: the carrier of S c= the carrier of L by Def13;
[y,z] in the InternalRel of S by A2;
then A4: z in the carrier of S by ZFMISC_1:87;
A5: [x,y] in the InternalRel of S by A1;
then A6: x in the carrier of S by ZFMISC_1:87;
y in the carrier of S by A5, ZFMISC_1:87;
then reconsider a = x, b = y, c = z as Element of L by A6, A4, A3;
( a <= b & b <= c ) by A1, A2, Th59;
hence x <= z by A6, Th60, ORDERS_2:3; :: thesis: verum