for S being TopStruct
for X being Subset of S st X is closed_under_lines & X is strong holds
X,X are_joinable