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

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 :: thesis: for x, y, z being object st x in X & y in X & z in X & [x,y] in R [*] & [y,z] in R [*] holds

[x,z] in R [*]

hence
R [*] is_transitive_in X
by RELAT_2:def 8; :: thesis: verum[x,z] in R [*]

let x, y, z be object ; :: thesis: ( x in X & y in X & z in X & [x,y] in R [*] & [y,z] in R [*] implies [x,z] in R [*] )

assume that

A2: x in X and

y in X and

z in X and

A3: ( [x,y] in R [*] & [y,z] in R [*] ) ; :: thesis: [x,z] in R [*]

( R reduces x,y & R reduces y,z ) by A3, REWRITE1:20;

hence [x,z] in R [*] by A1, A2, Th6, REWRITE1:16; :: thesis: verum

end;assume that

A2: x in X and

y in X and

z in X and

A3: ( [x,y] in R [*] & [y,z] in R [*] ) ; :: thesis: [x,z] in R [*]

( R reduces x,y & R reduces y,z ) by A3, REWRITE1:20;

hence [x,z] in R [*] by A1, A2, Th6, REWRITE1:16; :: thesis: verum