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;

hence R \~ is transitive ; :: thesis: verum

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 \~)

then
the InternalRel of (R \~) is_transitive_in the carrier of (R \~)
;[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;

end;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 ~

hence
[x,z] in the InternalRel of (R \~)
by A8, XBOOLE_0:def 5; :: thesis: verumassume
[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;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

hence R \~ is transitive ; :: thesis: verum