for TS being TopStruct
for K, K1, L, L1 being Subset of TS st K,L are_separated & K1 c= K & L1 c= L holds
K1,L1 are_separated