:: deftheorem defines connected PENCIL_1:def 10 :
for S being TopStruct holds
( S is connected iff for x, y being Point of S ex f being FinSequence of the carrier of S st
( x = f . 1 & y = f . (len f) & ( for i being Nat st 1 <= i & i < len f holds
for a, b being Point of S st a = f . i & b = f . (i + 1) holds
a,b are_collinear ) ) );