let X be set ; :: thesis: for R being Relation of X st R is_reflexive_in X holds
R [*] is_transitive_in X
let R be Relation of X; :: thesis: ( R is_reflexive_in X implies R [*] is_transitive_in X )
assume A1: R is_reflexive_in X ; :: thesis: R [*] is_transitive_in X

now

let x, y, z be set ; :: thesis: ( x in X & y in X & z in X & [x,y] in R [*] & [y,z] in R [*] implies [x,z] in R [*] )
assume A2: ( x in X & y in X & z in X & [x,y] in R [*] & [y,z] in R [*] ) ; :: thesis: [x,z] in R [*]
then A3: R reduces x,y by REWRITE1:21;
R reduces y,z by A2, REWRITE1:21;
hence [x,z] in R [*] by A1, A2, A3, Th6, REWRITE1:17; :: thesis: verum

end;

hence R [*] is_transitive_in X by RELAT_2:def 8; :: thesis: verum