let R be RelStr ; :: thesis: ( R is empty implies R is path-connected )
assume A1: R is empty ; :: thesis: R is path-connected
let x, y be set ; :: according to NECKLA_3:def 1 :: thesis: ( x in the carrier of R & y in the carrier of R & x <> y & not the InternalRel of R reduces x,y implies the InternalRel of R reduces y,x )
assume ( x in the carrier of R & y in the carrier of R & x <> y ) ; :: thesis: ( the InternalRel of R reduces x,y or the InternalRel of R reduces y,x )
hence ( the InternalRel of R reduces x,y or the InternalRel of R reduces y,x ) by A1; :: thesis: verum