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 )

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

suppose A <> [#] T ; :: thesis: ex C being Subset of T st
( 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

proof

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;

V is closed by A2, A5;
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;

suppose A14: A = [#] T ; :: thesis: ex C being Subset of T st
( C is open & B c= C & Cl C c= A )

take [#] T ; :: thesis: ( [#] T is open & B c= [#] T & Cl ([#] T) c= A )
thus ( [#] T is open & B c= [#] T & Cl ([#] T) c= A ) by A14; :: thesis: verum

end;

end;