for X being non empty set
for R being totally_connected Relation of X
for x, y being Element of X holds
( x <=_ R,y or y <=_ R,x ) by Rtot, RELAT_2:def 7;