theorem :: RELAT_2:31

for R being Relation holds
( R is transitive iff for x, y, z being object st [x,y] in R & [y,z] in R holds
[x,z] in R )