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 )

( 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

hence
( A \/ B is closed & A \/ C is closed )
by A1, A2, A3; :: thesis: verumA \/ 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;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