theorem :: ORDERS_1:11

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