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 :: thesis: for K, L being Subset of TS st K is open & L is open holds
K \ L,L \ K are_separated

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:23;
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:13;
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 `) = {} ;
K misses K ` by XBOOLE_1:79;
then A11: K /\ (K `) = {} ;
([#] TS) \ K = K ` ;
then A12: ((Cl K) /\ (Cl (L `))) /\ (L /\ (K `)) = ((Cl K) /\ (L `)) /\ (L /\ (K `)) by A3, PRE_TOPC:23;
A13: L \ K = L /\ (K `) by SUBSET_1:13;
Cl (L /\ (K `)) c= (Cl L) /\ (Cl (K `)) by PRE_TOPC:21;
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) ;
Cl (K /\ (L `)) c= (Cl K) /\ (Cl (L `)) by PRE_TOPC:21;
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 ;
hence K \ L,L \ K are_separated by A14; :: thesis: verum

end;

A15: now :: thesis: for K, L being Subset of TS st K is closed & L is closed holds
K \ L,L \ K are_separated

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 3;
A19: (([#] TS) \ K) \ (([#] TS) \ L) = (K `) /\ ((([#] TS) \ L) `) by SUBSET_1:13
.= (K `) /\ L by PRE_TOPC:3
.= L \ K by SUBSET_1:13 ;
A20: (([#] TS) \ L) \ (([#] TS) \ K) = (L `) /\ ((([#] TS) \ K) `) by SUBSET_1:13
.= (L `) /\ K by PRE_TOPC:3
.= K \ L by SUBSET_1:13 ;
([#] TS) \ K is open by A16, PRE_TOPC:def 3;
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