let GX be TopSpace; :: thesis: 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; :: thesis: ( ([#] 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 ; :: thesis: ( A \/ B is closed & A \/ C is closed )

now :: thesis: 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; :: thesis: ( ([#] 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 ; :: thesis: 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; :: thesis: verum

end;

hence ( A \/ B is closed & A \/ C is closed ) by A1, A2, A3; :: thesis: verum