theorem Th8: :: TAXONOM1:8

for X being set
for R being Relation of X st R is_reflexive_in X holds
R [*] is_transitive_in X