let R be Relation; :: thesis: ( R is transitive implies R \~ is transitive )
assume A1: R is transitive ; :: thesis: R \~ is transitive
A2: R is_transitive_in field R by A1, 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 \~ ) & y in field (R \~ ) & z in field (R \~ ) ) and
A3: [x,y] in R \~ and
A4: [y,z] in R \~ ; :: thesis: [x,z] in R \~
A5: ( x in field R & y in field R & z in field R ) by A3, A4, RELAT_1:30;
then A6: [x,z] in R by A2, A3, A4, RELAT_2:def 8;
not [x,y] in R ~ by A3, XBOOLE_0:def 5;
then not [y,x] in R by RELAT_1:def 7;
then not [z,x] in R by A2, A4, A5, RELAT_2:def 8;
then not [x,z] in R ~ by RELAT_1:def 7;
hence [x,z] in R \~ by A6, 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