let R be Relation; :: thesis: ( R is transitive implies R \~ is transitive )
assume R is transitive ; :: thesis: R \~ is transitive
then A1: R is_transitive_in field R by RELAT_2:def 16;

now

let x, y, z be set ; :: thesis: ( x in field (R \~) & y in field (R \~) & z in field (R \~) & [x,y] in R \~ & [y,z] in R \~ implies [x,z] in R \~ )
assume that
x in field (R \~) and
y in field (R \~) and
z in field (R \~) and
A2: [x,y] in R \~ and
A3: [y,z] in R \~ ; :: thesis: [x,z] in R \~
A4: x in field R by A2, RELAT_1:15;
A5: y in field R by A2, RELAT_1:15;
A6: z in field R by A3, RELAT_1:15;
then A7: [x,z] in R by A1, A2, A3, A4, A5, RELAT_2:def 8;
not [x,y] in R ~ by A2, XBOOLE_0:def 5;
then not [y,x] in R by RELAT_1:def 7;
then not [z,x] in R by A1, A3, A4, A5, A6, RELAT_2:def 8;
then not [x,z] in R ~ by RELAT_1:def 7;
hence [x,z] in R \~ by A7, XBOOLE_0:def 5; :: thesis: verum

end;

then R \~ is_transitive_in field (R \~) by RELAT_2:def 8;
hence R \~ is transitive by RELAT_2:def 16; :: thesis: verum