let N be non empty RelStr ; :: thesis: ( N is transitive iff RelStr(# the carrier of N, the InternalRel of N #) is transitive )
thus ( N is transitive implies RelStr(# the carrier of N, the InternalRel of N #) is transitive ) :: thesis: ( RelStr(# the carrier of N, the InternalRel of N #) is transitive implies N is transitive )

proof

assume A1: N is transitive ; :: thesis: RelStr(# the carrier of N, the InternalRel of N #) is transitive
let x, y, z be Element of RelStr(# the carrier of N, the InternalRel of N #); :: according to YELLOW_0:def 2 :: thesis: ( not x <= y or not y <= z or x <= z )
assume that
A2: x <= y and
A3: y <= z ; :: thesis: x <= z
reconsider x9 = x, y9 = y, z9 = z as Element of N ;
[y,z] in the InternalRel of RelStr(# the carrier of N, the InternalRel of N #) by A3, ORDERS_2:def 5;
then A4: y9 <= z9 by ORDERS_2:def 5;
[x,y] in the InternalRel of RelStr(# the carrier of N, the InternalRel of N #) by A2, ORDERS_2:def 5;
then x9 <= y9 by ORDERS_2:def 5;
then x9 <= z9 by A1, A4;
then [x9,z9] in the InternalRel of N by ORDERS_2:def 5;
hence x <= z by ORDERS_2:def 5; :: thesis: verum

end;

assume A5: RelStr(# the carrier of N, the InternalRel of N #) is transitive ; :: thesis: N is transitive
let x, y, z be Element of N; :: according to YELLOW_0:def 2 :: thesis: ( not x <= y or not y <= z or x <= z )
assume that
A6: x <= y and
A7: y <= z ; :: thesis: x <= z
reconsider x9 = x, y9 = y, z9 = z as Element of RelStr(# the carrier of N, the InternalRel of N #) ;
[y9,z9] in the InternalRel of RelStr(# the carrier of N, the InternalRel of N #) by A7, ORDERS_2:def 5;
then A8: y9 <= z9 by ORDERS_2:def 5;
[x9,y9] in the InternalRel of RelStr(# the carrier of N, the InternalRel of N #) by A6, ORDERS_2:def 5;
then x9 <= y9 by ORDERS_2:def 5;
then x9 <= z9 by A5, A8;
then [x,z] in the InternalRel of N by ORDERS_2:def 5;
hence x <= z by ORDERS_2:def 5; :: thesis: verum