for TS being TopStruct
for K, L being Subset of TS st ( ( K is closed & L is closed ) or ( K is open & L is open ) ) holds
K \ L,L \ K are_separated