:: deftheorem defines path-connected NECKLA_3:def 2 :
for R being symmetric 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 holds
the InternalRel of R reduces x,y );