theorem :: ORDERS_1:73

for R being Relation
for X being set st R is_transitive_in X holds
R |_2 X is transitive by Lm9;