let R be Relation of X; :: thesis: ( R is totally_connected implies R is strongly_connected )
assume AS: R is totally_connected ; :: thesis: R is strongly_connected
H: field R c= X \/ X by RELSET_1:8;

now :: thesis: for o1, o2 being object st o1 in field R & o2 in field R & not [o1,o2] in R holds
[o2,o1] in R

let o1, o2 be object ; :: thesis: ( o1 in field R & o2 in field R & not [b₁,b₂] in R implies [b₂,b₁] in R )
assume A: ( o1 in field R & o2 in field R ) ; :: thesis: ( [b₁,b₂] in R or [b₂,b₁] in R )
then reconsider x = o1, y = o2 as Element of X by H;

per cases ( X is empty or not X is empty ) ;

suppose X is empty ; :: thesis: ( [b₁,b₂] in R or [b₂,b₁] in R )

hence ( [o1,o2] in R or [o2,o1] in R ) by H, A; :: thesis: verum

end;

suppose not X is empty ; :: thesis: ( [b₁,b₂] in R or [b₂,b₁] in R )

then ( [x,y] in R or [y,x] in R ) by AS, RELAT_2:def 7;
hence ( [o1,o2] in R or [o2,o1] in R ) ; :: thesis: verum

end;

end;

end;

hence R is strongly_connected by RELAT_2:def 15, RELAT_2:def 7; :: thesis: verum