let A be transitive RelStr ; :: thesis: for a1, a2, a3 being Element of A st a1 <= a2 & a2 <= a3 holds
a1 <= a3
let a1, a2, a3 be Element of A; :: thesis: ( a1 <= a2 & a2 <= a3 implies a1 <= a3 )
assume A1: ( [a1,a2] in the InternalRel of A & [a2,a3] in the InternalRel of A ) ; :: according to ORDERS_2:def 9 :: thesis: a1 <= a3
then ( a1 in the carrier of A & a2 in the carrier of A & a3 in the carrier of A & the InternalRel of A is_transitive_in the carrier of A ) by Def5, ZFMISC_1:106;
hence [a1,a3] in the InternalRel of A by A1, RELAT_2:def 8; :: according to ORDERS_2:def 9 :: thesis: verum