let T be non empty TopSpace; :: thesis: ( T is normal implies for A, B being Subset of T st A is open & B is closed & B <> {} & B c= A holds

ex C being Subset of T st

( C is open & B c= C & Cl C c= A ) )

assume A1: T is normal ; :: thesis: for A, B being Subset of T st A is open & B is closed & B <> {} & B c= A holds

ex C being Subset of T st

( C is open & B c= C & Cl C c= A )

let A, B be Subset of T; :: thesis: ( A is open & B is closed & B <> {} & B c= A implies ex C being Subset of T st

( C is open & B c= C & Cl C c= A ) )

assume that

A2: A is open and

A3: ( B is closed & B <> {} ) and

A4: B c= A ; :: thesis: ex C being Subset of T st

( C is open & B c= C & Cl C c= A )

ex C being Subset of T st

( C is open & B c= C & Cl C c= A ) )

assume A1: T is normal ; :: thesis: for A, B being Subset of T st A is open & B is closed & B <> {} & B c= A holds

ex C being Subset of T st

( C is open & B c= C & Cl C c= A )

let A, B be Subset of T; :: thesis: ( A is open & B is closed & B <> {} & B c= A implies ex C being Subset of T st

( C is open & B c= C & Cl C c= A ) )

assume that

A2: A is open and

A3: ( B is closed & B <> {} ) and

A4: B c= A ; :: thesis: ex C being Subset of T st

( C is open & B c= C & Cl C c= A )

per cases
( A <> [#] T or A = [#] T )
;

end;

suppose
A <> [#] T
; :: thesis: ex C being Subset of T st

( C is open & B c= C & Cl C c= A )

( C is open & B c= C & Cl C c= A )

reconsider V = ([#] T) \ A as Subset of T ;

A5: A = ([#] T) \ V by PRE_TOPC:3;

A6: B misses V

then consider C, Q being Subset of T such that

A8: C is open and

A9: Q is open and

A10: B c= C and

A11: V c= Q and

A12: C misses Q by A1, A3, A6;

C c= Q ` by A12, SUBSET_1:23;

then Cl C c= Q ` by A9, TOPS_1:5;

then Q misses Cl C by SUBSET_1:23;

then A13: V misses Cl C by A11, XBOOLE_1:63;

take C ; :: thesis: ( C is open & B c= C & Cl C c= A )

thus ( C is open & B c= C ) by A8, A10; :: thesis: Cl C c= A

(A `) ` = A ;

hence Cl C c= A by A13, SUBSET_1:23; :: thesis: verum

end;A5: A = ([#] T) \ V by PRE_TOPC:3;

A6: B misses V

proof

V is closed
by A2, A5;
assume
B /\ V <> {}
; :: according to XBOOLE_0:def 7 :: thesis: contradiction

then consider z being object such that

A7: z in B /\ V by XBOOLE_0:def 1;

( z in B & z in V ) by A7, XBOOLE_0:def 4;

hence contradiction by A4, XBOOLE_0:def 5; :: thesis: verum

end;then consider z being object such that

A7: z in B /\ V by XBOOLE_0:def 1;

( z in B & z in V ) by A7, XBOOLE_0:def 4;

hence contradiction by A4, XBOOLE_0:def 5; :: thesis: verum

then consider C, Q being Subset of T such that

A8: C is open and

A9: Q is open and

A10: B c= C and

A11: V c= Q and

A12: C misses Q by A1, A3, A6;

C c= Q ` by A12, SUBSET_1:23;

then Cl C c= Q ` by A9, TOPS_1:5;

then Q misses Cl C by SUBSET_1:23;

then A13: V misses Cl C by A11, XBOOLE_1:63;

take C ; :: thesis: ( C is open & B c= C & Cl C c= A )

thus ( C is open & B c= C ) by A8, A10; :: thesis: Cl C c= A

(A `) ` = A ;

hence Cl C c= A by A13, SUBSET_1:23; :: thesis: verum