theorem :: ORDERS_1:78

for R being Relation st R is connected holds
R ~ is connected by Lm5;