set IR = the InternalRel of R;
set CR = the carrier of R;
set IR' = the InternalRel of (R \~ );
set CR' = 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 \~ ) & y in the carrier of (R \~ ) & z in the carrier of (R \~ ) ) and
A3: ( [x,y] in the InternalRel of (R \~ ) & [y,z] in the InternalRel of (R \~ ) ) ; :: thesis: [x,z] in the InternalRel of (R \~ )
A4: ( [x,y] in the InternalRel of R & not [x,y] in the InternalRel of R ~ & [y,z] in the InternalRel of R ) by A3, XBOOLE_0:def 5;
A5: [x,z] in the InternalRel of R by A1, A2, A3, 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, RELAT_2:def 8;
hence contradiction by A4, RELAT_1:def 7; :: thesis: verum

end;

hence [x,z] in the InternalRel of (R \~ ) by A5, 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