let TS be TopStruct ; :: thesis: for K, L being Subset of TS st K is closed & L is closed & K misses L holds
K,L are_separated
let K, L be Subset of TS; :: thesis: ( K is closed & L is closed & K misses L implies K,L are_separated )
assume that
A1: K is closed and
A2: L is closed and
A3: K misses L ; :: thesis: K,L are_separated
A4: K /\ L = {} by A3, XBOOLE_0:def 7;
K /\ (Cl L) = K /\ L by A2, PRE_TOPC:22;
then A5: K misses Cl L by A4, XBOOLE_0:def 7;
(Cl K) /\ L = K /\ L by A1, PRE_TOPC:22;
then Cl K misses L by A4, XBOOLE_0:def 7;
hence K,L are_separated by A5, Def1; :: thesis: verum