theorem :: PARTIT_2:27

for X being non empty set
for R being Relation of X st R is_transitive_in X holds
R is transitive