let A be transitive antisymmetric 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 & a2 < a3 ) ; :: thesis: a1 < a3
then ( a1 <= a2 & a2 <= a3 ) by Def10;
hence a1 <= a3 by Th26; :: according to ORDERS_2:def 10 :: thesis: a1 <> a3
thus a1 <> a3 by A1, Th28; :: thesis: verum