let X be non empty TopSpace; for A1, A2 being Subset of X holds
( A1,A2 are_weakly_separated iff ex C1, C2, C being Subset of X st
( C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C & C1 is open & C2 is open & C is closed ) )
let A1, A2 be Subset of X; ( A1,A2 are_weakly_separated iff ex C1, C2, C being Subset of X st
( C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C & C1 is open & C2 is open & C is closed ) )
set B1 = A1 \ A2;
set B2 = A2 \ A1;
A1:
(A1 \/ A2) ` misses A1 \/ A2
by XBOOLE_1:79;
thus
( A1,A2 are_weakly_separated implies ex C1, C2, C being Subset of X st
( C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C & C1 is open & C2 is open & C is closed ) )
( ex C1, C2, C being Subset of X st
( C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C & C1 is open & C2 is open & C is closed ) implies A1,A2 are_weakly_separated )proof
assume
A1,
A2 are_weakly_separated
;
ex C1, C2, C being Subset of X st
( C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C & C1 is open & C2 is open & C is closed )
then
A1 \ A2,
A2 \ A1 are_separated
;
then consider C1,
C2 being
Subset of
X such that A2:
(
A1 \ A2 c= C1 &
A2 \ A1 c= C2 )
and A3:
C1 misses A2 \ A1
and A4:
C2 misses A1 \ A2
and A5:
(
C1 is
open &
C2 is
open )
by Th44;
C1 /\ (A2 \ A1) = {}
by A3, XBOOLE_0:def 7;
then
(C1 /\ A2) \ (C1 /\ A1) = {}
by XBOOLE_1:50;
then A6:
C1 /\ A2 c= C1 /\ A1
by XBOOLE_1:37;
take
C1
;
ex C2, C being Subset of X st
( C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C & C1 is open & C2 is open & C is closed )
take
C2
;
ex C being Subset of X st
( C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C & C1 is open & C2 is open & C is closed )
take C =
(C1 \/ C2) ` ;
( C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C & C1 is open & C2 is open & C is closed )
(A1 \ A2) \/ (A2 \ A1) c= C1 \/ C2
by A2, XBOOLE_1:13;
then
C c= ((A1 \ A2) \/ (A2 \ A1)) `
by SUBSET_1:12;
then
C c= (A1 \+\ A2) `
by XBOOLE_0:def 6;
then
C c= ((A1 \/ A2) \ (A1 /\ A2)) `
by XBOOLE_1:101;
then
C c= ((A1 \/ A2) `) \/ (A1 /\ A2)
by SUBSET_1:14;
then
C /\ (A1 \/ A2) c= (((A1 \/ A2) `) \/ (A1 /\ A2)) /\ (A1 \/ A2)
by XBOOLE_1:26;
then
C /\ (A1 \/ A2) c= (((A1 \/ A2) `) /\ (A1 \/ A2)) \/ ((A1 /\ A2) /\ (A1 \/ A2))
by XBOOLE_1:23;
then A7:
C /\ (A1 \/ A2) c= ({} X) \/ ((A1 /\ A2) /\ (A1 \/ A2))
by A1, XBOOLE_0:def 7;
C2 /\ (A1 \ A2) = {}
by A4, XBOOLE_0:def 7;
then
(C2 /\ A1) \ (C2 /\ A2) = {}
by XBOOLE_1:50;
then A8:
C2 /\ A1 c= C2 /\ A2
by XBOOLE_1:37;
C2 /\ (A1 \/ A2) = (C2 /\ A1) \/ (C2 /\ A2)
by XBOOLE_1:23;
then A9:
C2 /\ (A1 \/ A2) = C2 /\ A2
by A8, XBOOLE_1:12;
C1 /\ (A1 \/ A2) = (C1 /\ A1) \/ (C1 /\ A2)
by XBOOLE_1:23;
then A10:
C1 /\ (A1 \/ A2) = C1 /\ A1
by A6, XBOOLE_1:12;
(
[#] X = (C `) \/ C &
(A1 /\ A2) /\ (A1 \/ A2) c= A1 /\ A2 )
by PRE_TOPC:2, XBOOLE_1:17;
hence
(
C1 /\ (A1 \/ A2) c= A1 &
C2 /\ (A1 \/ A2) c= A2 &
C /\ (A1 \/ A2) c= A1 /\ A2 & the
carrier of
X = (C1 \/ C2) \/ C &
C1 is
open &
C2 is
open &
C is
closed )
by A5, A10, A9, A7, XBOOLE_1:1, XBOOLE_1:17;
verum
end;
given C1, C2, C being Subset of X such that A11:
C1 /\ (A1 \/ A2) c= A1
and
A12:
C2 /\ (A1 \/ A2) c= A2
and
A13:
C /\ (A1 \/ A2) c= A1 /\ A2
and
A14:
the carrier of X = (C1 \/ C2) \/ C
and
A15:
( C1 is open & C2 is open )
and
C is closed
; A1,A2 are_weakly_separated
ex C1, C2 being Subset of X st
( A1 \ A2 c= C1 & A2 \ A1 c= C2 & C1 /\ C2 misses (A1 \ A2) \/ (A2 \ A1) & C1 is open & C2 is open )
proof
(C1 /\ (A1 \/ A2)) /\ (C2 /\ (A1 \/ A2)) c= A1 /\ A2
by A11, A12, XBOOLE_1:27;
then
(C1 /\ ((A1 \/ A2) /\ C2)) /\ (A1 \/ A2) c= A1 /\ A2
by XBOOLE_1:16;
then
((C1 /\ C2) /\ (A1 \/ A2)) /\ (A1 \/ A2) c= A1 /\ A2
by XBOOLE_1:16;
then
(C1 /\ C2) /\ ((A1 \/ A2) /\ (A1 \/ A2)) c= A1 /\ A2
by XBOOLE_1:16;
then
((C1 /\ C2) /\ (A1 \/ A2)) \ (A1 /\ A2) = {}
by XBOOLE_1:37;
then
(C1 /\ C2) /\ ((A1 \/ A2) \ (A1 /\ A2)) = {}
by XBOOLE_1:49;
then A16:
(C1 /\ C2) /\ ((A1 \ A2) \/ (A2 \ A1)) = {}
by XBOOLE_1:55;
A1 /\ A2 c= A2
by XBOOLE_1:17;
then
C /\ (A1 \/ A2) c= A2
by A13, XBOOLE_1:1;
then
(C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) c= A2
by A12, XBOOLE_1:8;
then A17:
(C2 \/ C) /\ (A1 \/ A2) c= A2
by XBOOLE_1:23;
A1 c= A1 \/ A2
by XBOOLE_1:7;
then
A1 \ A2 c= (A1 \/ A2) \ ((C2 \/ C) /\ (A1 \/ A2))
by A17, XBOOLE_1:35;
then A18:
A1 \ A2 c= (A1 \/ A2) \ (C2 \/ C)
by XBOOLE_1:47;
A1 /\ A2 c= A1
by XBOOLE_1:17;
then
C /\ (A1 \/ A2) c= A1
by A13, XBOOLE_1:1;
then
(C /\ (A1 \/ A2)) \/ (C1 /\ (A1 \/ A2)) c= A1
by A11, XBOOLE_1:8;
then A19:
(C \/ C1) /\ (A1 \/ A2) c= A1
by XBOOLE_1:23;
A2 c= A1 \/ A2
by XBOOLE_1:7;
then
A2 \ A1 c= (A1 \/ A2) \ ((C \/ C1) /\ (A1 \/ A2))
by A19, XBOOLE_1:35;
then A20:
A2 \ A1 c= (A1 \/ A2) \ (C \/ C1)
by XBOOLE_1:47;
take
C1
;
ex C2 being Subset of X st
( A1 \ A2 c= C1 & A2 \ A1 c= C2 & C1 /\ C2 misses (A1 \ A2) \/ (A2 \ A1) & C1 is open & C2 is open )
take
C2
;
( A1 \ A2 c= C1 & A2 \ A1 c= C2 & C1 /\ C2 misses (A1 \ A2) \/ (A2 \ A1) & C1 is open & C2 is open )
A21:
A1 \/ A2 c= [#] X
;
then
A1 \/ A2 c= (C2 \/ C) \/ C1
by A14, XBOOLE_1:4;
then A22:
(A1 \/ A2) \ (C2 \/ C) c= C1
by XBOOLE_1:43;
A1 \/ A2 c= (C \/ C1) \/ C2
by A14, A21, XBOOLE_1:4;
then
(A1 \/ A2) \ (C \/ C1) c= C2
by XBOOLE_1:43;
hence
(
A1 \ A2 c= C1 &
A2 \ A1 c= C2 &
C1 /\ C2 misses (A1 \ A2) \/ (A2 \ A1) &
C1 is
open &
C2 is
open )
by A15, A20, A18, A22, A16, XBOOLE_0:def 7, XBOOLE_1:1;
verum
end;
then
A1 \ A2,A2 \ A1 are_separated
by Th45;
hence
A1,A2 are_weakly_separated
; verum