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 A5: 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 ;
A6: A = ([#] T) \ V by PRE_TOPC:22;
then A7: ([#] T) \ A <> {} by A5;
A8: B misses V

proof

assume B /\ V <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider z being set such that
A9: z in B /\ V by XBOOLE_0:def 1;
( z in B & z in V ) by A9, XBOOLE_0:def 4;
hence contradiction by A4, XBOOLE_0:def 5; :: thesis: verum

end;

V is closed by A2, A6, PRE_TOPC:def 6;
then consider C, Q being Subset of T such that
A10: C is open and
A11: Q is open and
A12: B c= C and
A13: V c= Q and
A14: C misses Q by A1, A3, A7, A8, COMPTS_1:def 6;
C c= Q ` by A14, SUBSET_1:43;
then Cl C c= Q ` by A11, TOPS_1:31;
then Q misses Cl C by SUBSET_1:43;
then A15: V misses Cl C by A13, XBOOLE_1:63;
take C ; :: thesis: ( C is open & B c= C & Cl C c= A )
thus ( C is open & B c= C ) by A10, A12; :: thesis: Cl C c= A
(A ` ) ` = A ;
hence Cl C c= A by A15, SUBSET_1:43; :: thesis: verum

end;

suppose A16: 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 A16; :: thesis: verum

end;

end;