theorem :: ORDERS_1:82

for R being Relation
for X being set st R is_connected_in X holds
R ~ is_connected_in X by Lm15;