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

A1: now

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
A2: ([#] GX) \ A = B \/ C and
A3: B,C are_separated and
A4: A is closed ; :: thesis: A \/ B is closed
A5: Cl A = A by A4, PRE_TOPC:52;
A6: [#] GX = A \/ (B \/ C) by A2, XBOOLE_1:45;
( Cl B misses C & B misses Cl C ) by A3, Def1;
then A7: ( (Cl B) /\ C = {} & B /\ (Cl C) = {} ) by XBOOLE_0:def 7;
Cl (A \/ B) = (Cl A) \/ (Cl B) by PRE_TOPC:50
.= A \/ ((Cl B) /\ (A \/ (B \/ C))) by A5, A6, 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 A7, PRE_TOPC:48, XBOOLE_1:28 ;
hence A \/ B is closed by PRE_TOPC:52; :: thesis: verum

end;

assume that
A8: ([#] GX) \ A = B \/ C and
A9: B,C are_separated and
A10: A is closed ; :: thesis: ( A \/ B is closed & A \/ C is closed )
thus ( A \/ B is closed & A \/ C is closed ) by A1, A8, A9, A10; :: thesis: verum