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 )

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

hence
R is connected
by WAYBEL_0:def 29; :: thesis: verum
let x, y be Element of R; :: thesis: ( x <= y or y <= x )

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

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;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