:: deftheorem defines path-connected NECKLA_3:def 1 :
for R being RelStr holds
( R is path-connected iff 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 );