theorem :: ORDERS_1:76

for R being Relation
for X, Y being set st R is_connected_in X & Y c= X holds
R is_connected_in Y ;