let GX be TopSpace; for A, B, C being Subset of GX st ([#] GX) \ A = B \/ C & B,C are_separated & A is closed holds
( A \/ B is closed & A \/ C is closed )
let A, B, C be Subset of GX; ( ([#] GX) \ A = B \/ C & B,C are_separated & A is closed implies ( A \/ B is closed & A \/ C is closed ) )
assume that
A1:
([#] GX) \ A = B \/ C
and
A2:
B,C are_separated
and
A3:
A is closed
; ( A \/ B is closed & A \/ C is closed )
now for A, B, C being Subset of GX st ([#] GX) \ A = B \/ C & B,C are_separated & A is closed holds
A \/ B is closed let A,
B,
C be
Subset of
GX;
( ([#] GX) \ A = B \/ C & B,C are_separated & A is closed implies A \/ B is closed )assume that A4:
([#] GX) \ A = B \/ C
and A5:
B,
C are_separated
and A6:
A is
closed
;
A \/ B is closed A7:
Cl A = A
by A6, PRE_TOPC:22;
Cl B misses C
by A5;
then A8:
(Cl B) /\ C = {}
;
A9:
[#] GX = A \/ (B \/ C)
by A4, XBOOLE_1:45;
Cl (A \/ B) =
(Cl A) \/ (Cl B)
by PRE_TOPC:20
.=
A \/ ((Cl B) /\ (A \/ (B \/ C)))
by A7, A9, XBOOLE_1:28
.=
(A \/ (Cl B)) /\ (A \/ (A \/ (B \/ C)))
by XBOOLE_1:24
.=
(A \/ (Cl B)) /\ ((A \/ A) \/ (B \/ C))
by XBOOLE_1:4
.=
A \/ ((Cl B) /\ (B \/ C))
by XBOOLE_1:24
.=
A \/ (((Cl B) /\ B) \/ ((Cl B) /\ C))
by XBOOLE_1:23
.=
A \/ B
by A8, PRE_TOPC:18, XBOOLE_1:28
;
hence
A \/ B is
closed
by PRE_TOPC:22;
verum end;
hence
( A \/ B is closed & A \/ C is closed )
by A1, A2, A3; verum