theorem :: PARTIT_2:26

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