let R be non empty reflexive transitive RelStr ; :: thesis: ( R is path-connected implies R is connected )
set IR = the InternalRel of R;
assume A1: R is path-connected ; :: thesis: R is connected
for x, y being Element of R holds
( x <= y or y <= x )

proof

let x, y be Element of R; :: thesis: ( x <= y or y <= x )

per cases ( x = y or x <> y ) ;

suppose x = y ; :: thesis: ( x <= y or y <= x )

hence ( x <= y or y <= x ) ; :: thesis: verum

end;

suppose x <> y ; :: thesis: ( x <= y or y <= x )

then ( the InternalRel of R reduces x,y or the InternalRel of R reduces y,x ) by A1;
then ( [x,y] in the InternalRel of R or [y,x] in the InternalRel of R ) by Th26;
hence ( x <= y or y <= x ) by ORDERS_2:def 5; :: thesis: verum

end;

end;

end;

hence R is connected by WAYBEL_0:def 29; :: thesis: verum