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

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 ( x in field (R ~ ) & y in field (R ~ ) & z in field (R ~ ) & [x,y] in R ~ & [y,z] in R ~ ) ; :: thesis: [x,z] in R ~
then ( x in field R & y in field R & z in field R & [z,y] in R & [y,x] in R ) by RELAT_1:38, RELAT_1:def 7;
then [z,x] in R by A1, Def8;
hence [x,z] in R ~ by RELAT_1:def 7; :: thesis: verum

end;

then R ~ is_transitive_in field (R ~ ) by Def8;
hence R ~ is transitive by Def16; :: thesis: verum