let A be transitive antisymmetric RelStr ; :: thesis: for a1, a2, a3 being Element of A st ( ( a1 < a2 & a2 <= a3 ) or ( a1 <= a2 & a2 < a3 ) ) holds
a1 < a3
let a1, a2, a3 be Element of A; :: thesis: ( ( ( a1 < a2 & a2 <= a3 ) or ( a1 <= a2 & a2 < a3 ) ) implies a1 < a3 )

A1: now :: thesis: ( a1 < a2 & a2 <= a3 & ( ( a1 < a2 & a2 <= a3 ) or ( a1 <= a2 & a2 < a3 ) ) implies a1 < a3 )

assume that
A2: a1 < a2 and
A3: a2 <= a3 ; :: thesis: ( ( ( a1 < a2 & a2 <= a3 ) or ( a1 <= a2 & a2 < a3 ) ) implies a1 < a3 )
a1 <= a2 by A2, Def6;
then ( a1 <= a3 & a1 <> a3 ) by A2, A3, Th2, Th3;
hence ( ( ( a1 < a2 & a2 <= a3 ) or ( a1 <= a2 & a2 < a3 ) ) implies a1 < a3 ) by Def6; :: thesis: verum

end;

A4: now :: thesis: ( a1 <= a2 & a2 < a3 & ( ( a1 < a2 & a2 <= a3 ) or ( a1 <= a2 & a2 < a3 ) ) implies a1 < a3 )

assume that
A5: a1 <= a2 and
A6: a2 < a3 ; :: thesis: ( ( ( a1 < a2 & a2 <= a3 ) or ( a1 <= a2 & a2 < a3 ) ) implies a1 < a3 )
a2 <= a3 by A6, Def6;
then ( a1 <= a3 & a1 <> a3 ) by A5, A6, Th2, Th3;
hence ( ( ( a1 < a2 & a2 <= a3 ) or ( a1 <= a2 & a2 < a3 ) ) implies a1 < a3 ) by Def6; :: thesis: verum

end;

assume ( ( a1 < a2 & a2 <= a3 ) or ( a1 <= a2 & a2 < a3 ) ) ; :: thesis: a1 < a3
hence a1 < a3 by A1, A4; :: thesis: verum