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