for TS being TopStruct
for K, L being Subset of TS st K is closed & L is closed & K misses L holds
K,L are_separated by PRE_TOPC:22;