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

proof

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 A2: ( x in the carrier of R & y in the carrier of R & 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 9;

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

then A4: <*x,y*> is RedSequence of the InternalRel of R by REWRITE1:8;
( len <*x,y*> = 2 & <*x,y*> . 1 = x & <*x,y*> . 2 = y ) by FINSEQ_1:61;
hence ( the InternalRel of R reduces x,y or the InternalRel of R reduces y,x ) by A4, REWRITE1:def 3; :: thesis: verum

end;

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

then A5: <*y,x*> is RedSequence of the InternalRel of R by REWRITE1:8;
( len <*y,x*> = 2 & <*y,x*> . 1 = y & <*y,x*> . 2 = x ) by FINSEQ_1:61;
hence ( the InternalRel of R reduces x,y or the InternalRel of R reduces y,x ) by A5, REWRITE1:def 3; :: thesis: verum

end;

end;

end;

hence R is path-connected by Def1; :: thesis: verum