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;
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:
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 ; :: thesis: verum