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 )
assume A1: ( ( K is closed & L is closed ) or ( K is open & L is open ) ) ; :: thesis: K \ L,L \ K are_separated

A2: now

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

end;

now

let K, L be Subset of TS; :: thesis: ( K is closed & L is closed implies K \ L,L \ K are_separated )
assume ( K is closed & L is closed ) ; :: thesis: K \ L,L \ K are_separated
then A11: ( ([#] TS) \ K is open & ([#] TS) \ L is open ) by PRE_TOPC:def 6;
A12: (([#] 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) \ (([#] TS) \ L) = (K ` ) /\ ((([#] TS) \ L) ` ) by SUBSET_1:32
.= (K ` ) /\ L by PRE_TOPC:22
.= L \ K by SUBSET_1:32 ;
hence K \ L,L \ K are_separated by A2, A11, A12; :: thesis: verum

end;

hence K \ L,L \ K are_separated by A1, A2; :: thesis: verum