:: deftheorem Def8 defines is_transitive_in RELAT_2:def 8 :
for R being Relation
for X being set holds
( R is_transitive_in X iff 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 );