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