:: deftheorem defines are_joinable PENCIL_2:def 3 :
for S being TopStruct
for X, Y being Subset of S holds
( X,Y are_joinable iff ex f being 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))) ) ) );