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 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;
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;
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;
end;
end;
hence R is path-connected ; :: thesis: verum