:: deftheorem Rtot defines totally_connected REALALG1:def 2 :
for X being set
for R being Relation of X holds
( R is totally_connected iff R is_strongly_connected_in X );