theorem :: ORDERS_1:75

for R being Relation
for X being set st R is_connected_in X holds
R |_2 X is connected by Lm11;