set IR = the InternalRel of R;
set CR = the carrier of R;
set IR9 = the InternalRel of (R \~ );
set CR9 = the carrier of (R \~ );
A1: the InternalRel of R is_transitive_in the carrier of R by ORDERS_2:def 5;

now

let x, y, z be set ; :: thesis: ( x in the carrier of (R \~ ) & y in the carrier of (R \~ ) & z in the carrier of (R \~ ) & [x,y] in the InternalRel of (R \~ ) & [y,z] in the InternalRel of (R \~ ) implies [x,z] in the InternalRel of (R \~ ) )
assume that
A2: x in the carrier of (R \~ ) and
A3: y in the carrier of (R \~ ) and
A4: z in the carrier of (R \~ ) and
A5: [x,y] in the InternalRel of (R \~ ) and
A6: [y,z] in the InternalRel of (R \~ ) ; :: thesis: [x,z] in the InternalRel of (R \~ )
A7: not [x,y] in the InternalRel of R ~ by A5, XBOOLE_0:def 5;
A8: [x,z] in the InternalRel of R by A1, A2, A3, A4, A5, A6, RELAT_2:def 8;

now

assume [x,z] in the InternalRel of R ~ ; :: thesis: contradiction
then [z,x] in the InternalRel of R by RELAT_1:def 7;
then [y,x] in the InternalRel of R by A1, A2, A3, A4, A6, RELAT_2:def 8;
hence contradiction by A7, RELAT_1:def 7; :: thesis: verum

end;

hence [x,z] in the InternalRel of (R \~ ) by A8, XBOOLE_0:def 5; :: thesis: verum

end;

then the InternalRel of (R \~ ) is_transitive_in the carrier of (R \~ ) by RELAT_2:def 8;
hence R \~ is transitive by ORDERS_2:def 5; :: thesis: verum