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 that
A2: x in the carrier of R and
y in the carrier of R and
x <> y ; :: thesis: ( the InternalRel of R reduces x,y or the InternalRel of R reduces y,x )
thus ( the InternalRel of R reduces x,y or the InternalRel of R reduces y,x ) by A1, A2; :: thesis: verum