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 )

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

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

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;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

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

K \ L,L \ K are_separated

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

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