set IR = the InternalRel of R;
set cR = the carrier of R;
thus ( R is path-connected implies for x, y being set st x in the carrier of R & y in the carrier of R & x <> y holds
the InternalRel of R reduces x,y ) :: thesis: ( ( for x, y being set st x in the carrier of R & y in the carrier of R & x <> y holds
the InternalRel of R reduces x,y ) implies R is path-connected )

proof

assume A1: R is path-connected ; :: thesis: for x, y being set st x in the carrier of R & y in the carrier of R & x <> y holds
the InternalRel of R reduces x,y
let x, y be set ; :: thesis: ( x in the carrier of R & y in the carrier of R & x <> y implies the InternalRel of R reduces x,y )
assume A2: ( x in the carrier of R & y in the carrier of R & x <> y ) ; :: thesis: the InternalRel of R reduces x,y

per cases ( the InternalRel of R reduces x,y or the InternalRel of R reduces y,x ) by A1, A2, Def1;

suppose the InternalRel of R reduces x,y ; :: thesis: the InternalRel of R reduces x,y

hence the InternalRel of R reduces x,y ; :: thesis: verum

end;

suppose the InternalRel of R reduces y,x ; :: thesis: the InternalRel of R reduces x,y

hence the InternalRel of R reduces x,y by Th27; :: thesis: verum

end;

end;

end;

assume for x, y being set st x in the carrier of R & y in the carrier of R & x <> y holds
the InternalRel of R reduces x,y ; :: thesis: R is path-connected
then 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 ;
hence R is path-connected by Def1; :: thesis: verum