theorem :: ORDERS_1:10

for X, Y being set
for P being Relation st P is_transitive_in X & Y c= X holds
P is_transitive_in Y ;