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 )

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

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
for x, y being set st x in the carrier of R & y in the carrier of R & x <> y holds
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

end;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;

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