let R be non empty RelStr ; :: thesis: ( R is connected implies R is path-connected )

set cR = the carrier of R;

set IR = the InternalRel of R;

assume A1: R is connected ; :: thesis: R is path-connected

for x, y being set st x in the carrier of R & y in the carrier of R & x <> y & not the InternalRel of R reduces x,y holds

the InternalRel of R reduces y,x

set cR = the carrier of R;

set IR = the InternalRel of R;

assume A1: R is connected ; :: thesis: R is path-connected

for x, y being set st x in the carrier of R & y in the carrier of R & x <> y & not the InternalRel of R reduces x,y holds

the InternalRel of R reduces y,x

proof

hence
R is path-connected
; :: thesis: verum
let x, y be set ; :: thesis: ( x in the carrier of R & y in the carrier of R & x <> y & not the InternalRel of R reduces x,y implies the InternalRel of R reduces y,x )

assume that

A2: ( x in the carrier of R & y in the carrier of R ) and

x <> y ; :: thesis: ( the InternalRel of R reduces x,y or the InternalRel of R reduces y,x )

reconsider x = x, y = y as Element of R by A2;

A3: ( x <= y or y <= x ) by A1, WAYBEL_0:def 29;

end;assume that

A2: ( x in the carrier of R & y in the carrier of R ) and

x <> y ; :: thesis: ( the InternalRel of R reduces x,y or the InternalRel of R reduces y,x )

reconsider x = x, y = y as Element of R by A2;

A3: ( x <= y or y <= x ) by A1, WAYBEL_0:def 29;

per cases
( [x,y] in the InternalRel of R or [y,x] in the InternalRel of R )
by A3, ORDERS_2:def 5;

end;

suppose A4:
[x,y] in the InternalRel of R
; :: thesis: ( the InternalRel of R reduces x,y or the InternalRel of R reduces y,x )

A5:
( len <*x,y*> = 2 & <*x,y*> . 1 = x )
by FINSEQ_1:44;

A6: <*x,y*> . 2 = y by FINSEQ_1:44;

<*x,y*> is RedSequence of the InternalRel of R by A4, REWRITE1:7;

hence ( the InternalRel of R reduces x,y or the InternalRel of R reduces y,x ) by A5, A6, REWRITE1:def 3; :: thesis: verum

end;A6: <*x,y*> . 2 = y by FINSEQ_1:44;

<*x,y*> is RedSequence of the InternalRel of R by A4, REWRITE1:7;

hence ( the InternalRel of R reduces x,y or the InternalRel of R reduces y,x ) by A5, A6, REWRITE1:def 3; :: thesis: verum

suppose A7:
[y,x] in the InternalRel of R
; :: thesis: ( the InternalRel of R reduces x,y or the InternalRel of R reduces y,x )

A8:
( len <*y,x*> = 2 & <*y,x*> . 1 = y )
by FINSEQ_1:44;

A9: <*y,x*> . 2 = x by FINSEQ_1:44;

<*y,x*> is RedSequence of the InternalRel of R by A7, REWRITE1:7;

hence ( the InternalRel of R reduces x,y or the InternalRel of R reduces y,x ) by A8, A9, REWRITE1:def 3; :: thesis: verum

end;A9: <*y,x*> . 2 = x by FINSEQ_1:44;

<*y,x*> is RedSequence of the InternalRel of R by A7, REWRITE1:7;

hence ( the InternalRel of R reduces x,y or the InternalRel of R reduces y,x ) by A8, A9, REWRITE1:def 3; :: thesis: verum