let A be transitive RelStr ; for a1, a2, a3 being Element of A st a1 <= a2 & a2 <= a3 holds
a1 <= a3
let a1, a2, a3 be Element of A; ( a1 <= a2 & a2 <= a3 implies a1 <= a3 )
assume that
A1:
[a1,a2] in the InternalRel of A
and
A2:
[a2,a3] in the InternalRel of A
; ORDERS_2:def 5 a1 <= a3
A3:
the InternalRel of A is_transitive_in the carrier of A
by Def3;
a1 in the carrier of A
by A1, ZFMISC_1:87;
hence
[a1,a3] in the InternalRel of A
by A1, A2, A3; ORDERS_2:def 5 verum