for TS being TopStruct
for K, L being Subset of TS st K,L are_separated holds
K misses L