theorem Th7: :: EQREL_1:7

for X being set
for z being object
for R being transitive total Relation of X
for x, y being object st [x,y] in R & [y,z] in R holds
[x,z] in R