let TS be TopStruct ; :: thesis: for K, L being Subset of TS st K,L are_separated holds
K misses L
let K, L be Subset of TS; :: thesis: ( K,L are_separated implies K misses L )
assume A1: ( (Cl K) /\ L = {} & K /\ (Cl L) = {} ) ; :: according to XBOOLE_0:def 7,CONNSP_1:def 1 :: thesis: K misses L
( K c= Cl K & L c= L ) by PRE_TOPC:48;
hence K /\ L = {} by A1, XBOOLE_1:3, XBOOLE_1:27; :: according to XBOOLE_0:def 7 :: thesis: verum