let R be Relation of X; :: thesis: ( R is totally_connected implies not R is empty )
assume R is totally_connected ; :: thesis: not R is empty
then for x, y being Element of X holds
( [x,y] in R or [y,x] in R ) by RELAT_2:def 7;
hence not R is empty ; :: thesis: verum