let L1, L2 be RelStr ; :: thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is transitive implies L2 is transitive )
assume that
A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and
A2: L1 is transitive ; :: thesis: L2 is transitive

now

let x, y, z be Element of L2; :: thesis: ( x <= y & y <= z implies x <= z )
reconsider x9 = x, y9 = y, z9 = z as Element of L1 by A1;
assume ( x <= y & y <= z ) ; :: thesis: x <= z
then ( x9 <= y9 & y9 <= z9 ) by A1, YELLOW_0:1;
then x9 <= z9 by A2, YELLOW_0:def 2;
hence x <= z by A1, YELLOW_0:1; :: thesis: verum

end;

hence L2 is transitive by YELLOW_0:def 2; :: thesis: verum