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 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 ;
( 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 \~)
;
[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;
hence
[x,z] in the
InternalRel of
(R \~)
by A8, XBOOLE_0:def 5;
verum end;
then
the InternalRel of (R \~) is_transitive_in the carrier of (R \~)
;
hence
R \~ is transitive
; verum