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 3;

now :: thesis: for x, y, z being object st 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 \~) holds
[x,z] in the InternalRel of (R \~)

let x, y, z be object ; :: 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;

now :: thesis: not [x,z] in the InternalRel of R ~

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;
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 \~) ;
hence R \~ is transitive ; :: thesis: verum