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 that
A1: (Cl K) /\ L = {} and
K /\ (Cl L) = {} ; :: according to XBOOLE_0:def 7,CONNSP_1:def 1 :: thesis: K misses L
K c= Cl K by PRE_TOPC:18;
hence K /\ L = {} by A1, XBOOLE_1:3, XBOOLE_1:27; :: according to XBOOLE_0:def 7 :: thesis: verum