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

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