theorem :: PENCIL_2:9

for S being TopStruct
for X, Y being Subset of S st X,Y are_joinable holds
ex f being one-to-one FinSequence of bool the carrier of S st
( X = f . 1 & Y = f . (len f) & ( for W being Subset of S st W in rng f holds
( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len f holds
2 c= card ((f . i) /\ (f . (i + 1))) ) )