let TS be TopStruct ; :: thesis: for K, L being Subset of TS st ( ( K is closed & L is closed ) or ( K is open & L is open ) ) holds
K \ L,L \ K are_separated
let K, L be Subset of TS; :: thesis: ( ( ( K is closed & L is closed ) or ( K is open & L is open ) ) implies K \ L,L \ K are_separated )

A1: now

let K, L be Subset of TS; :: thesis: ( K is open & L is open implies K \ L,L \ K are_separated )
assume that
A2: K is open and
A3: L is open ; :: thesis: K \ L,L \ K are_separated
A4: K /\ (L ` ) c= K by XBOOLE_1:17;
A5: (Cl L) /\ (K ` ) c= K ` by XBOOLE_1:17;
Cl (([#] TS) \ K) = ([#] TS) \ K by A2, PRE_TOPC:53;
then A6: (K /\ (L ` )) /\ ((Cl L) /\ (Cl (K ` ))) c= K /\ (K ` ) by A4, A5, XBOOLE_1:27;
A7: K \ L = K /\ (L ` ) by SUBSET_1:32;
A8: L /\ (K ` ) c= L by XBOOLE_1:17;
(Cl K) /\ (L ` ) c= L ` by XBOOLE_1:17;
then A9: ((Cl K) /\ (L ` )) /\ (L /\ (K ` )) c= L /\ (L ` ) by A8, XBOOLE_1:27;
L misses L ` by XBOOLE_1:79;
then A10: L /\ (L ` ) = {} by XBOOLE_0:def 7;
K misses K ` by XBOOLE_1:79;
then A11: K /\ (K ` ) = {} by XBOOLE_0:def 7;
([#] TS) \ K = K ` ;
then A12: ((Cl K) /\ (Cl (L ` ))) /\ (L /\ (K ` )) = ((Cl K) /\ (L ` )) /\ (L /\ (K ` )) by A3, PRE_TOPC:53;
A13: L \ K = L /\ (K ` ) by SUBSET_1:32;
Cl (L /\ (K ` )) c= (Cl L) /\ (Cl (K ` )) by PRE_TOPC:51;
then (K \ L) /\ (Cl (L \ K)) c= (K /\ (L ` )) /\ ((Cl L) /\ (Cl (K ` ))) by A7, A13, XBOOLE_1:27;
then (K \ L) /\ (Cl (L \ K)) = {} TS by A11, A6;
then A14: K \ L misses Cl (L \ K) by XBOOLE_0:def 7;
Cl (K /\ (L ` )) c= (Cl K) /\ (Cl (L ` )) by PRE_TOPC:51;
then (Cl (K \ L)) /\ (L \ K) c= ((Cl K) /\ (Cl (L ` ))) /\ (L /\ (K ` )) by A7, A13, XBOOLE_1:27;
then (Cl (K \ L)) /\ (L \ K) = {} TS by A12, A10, A9;
then Cl (K \ L) misses L \ K by XBOOLE_0:def 7;
hence K \ L,L \ K are_separated by A14, Def1; :: thesis: verum

end;

A15: now

let K, L be Subset of TS; :: thesis: ( K is closed & L is closed implies K \ L,L \ K are_separated )
assume that
A16: K is closed and
A17: L is closed ; :: thesis: K \ L,L \ K are_separated
A18: ([#] TS) \ L is open by A17, PRE_TOPC:def 6;
A19: (([#] TS) \ K) \ (([#] TS) \ L) = (K ` ) /\ ((([#] TS) \ L) ` ) by SUBSET_1:32
.= (K ` ) /\ L by PRE_TOPC:22
.= L \ K by SUBSET_1:32 ;
A20: (([#] TS) \ L) \ (([#] TS) \ K) = (L ` ) /\ ((([#] TS) \ K) ` ) by SUBSET_1:32
.= (L ` ) /\ K by PRE_TOPC:22
.= K \ L by SUBSET_1:32 ;
([#] TS) \ K is open by A16, PRE_TOPC:def 6;
hence K \ L,L \ K are_separated by A1, A18, A20, A19; :: thesis: verum

end;

assume ( ( K is closed & L is closed ) or ( K is open & L is open ) ) ; :: thesis: K \ L,L \ K are_separated
hence K \ L,L \ K are_separated by A1, A15; :: thesis: verum