let T be non empty TopSpace; :: thesis: ( T is normal implies for A, B being open Subset of T st A <> {} & Cl A c= B holds
ex C being Subset of T st
( C <> {} & C is open & Cl A c= C & Cl C c= B ) )
assume A1: T is normal ; :: thesis: for A, B being open Subset of T st A <> {} & Cl A c= B holds
ex C being Subset of T st
( C <> {} & C is open & Cl A c= C & Cl C c= B )
let A, B be open Subset of T; :: thesis: ( A <> {} & Cl A c= B implies ex C being Subset of T st
( C <> {} & C is open & Cl A c= C & Cl C c= B ) )
assume A2: ( A <> {} & Cl A c= B ) ; :: thesis: ex C being Subset of T st
( C <> {} & C is open & Cl A c= C & Cl C c= B )

now

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

case A3: B <> [#] T ; :: thesis: ex C, C being Subset of T st
( C <> {} & C is open & Cl A c= C & Cl C c= B )

reconsider W = Cl A, V = ([#] T) \ B as Subset of T ;
B = ([#] T) \ V by PRE_TOPC:22;
then A4: V is closed by PRE_TOPC:def 6;
A5: ( W <> {} & V <> {} )

proof

consider x being set such that
A6: x in A by A2, XBOOLE_0:def 1;
A7: A c= Cl A by PRE_TOPC:48;
([#] T) \ B <> {}

proof

assume ([#] T) \ B = {} ; :: thesis: contradiction
then B = ([#] T) \ {} by PRE_TOPC:22;
hence contradiction by A3; :: thesis: verum

end;

hence ( W <> {} & V <> {} ) by A6, A7; :: thesis: verum

end;

W misses V

proof

assume W meets V ; :: thesis: contradiction
then consider x being set such that
A8: x in W /\ V by XBOOLE_0:4;
( x in Cl A & x in ([#] T) \ B ) by A8, XBOOLE_0:def 4;
hence contradiction by A2, XBOOLE_0:def 5; :: thesis: verum

end;

then consider C, Q being Subset of T such that
A9: ( C is open & Q is open & W c= C & V c= Q & C misses Q ) by A1, A4, A5, COMPTS_1:def 6;
take C = C; :: thesis: ex C being Subset of T st
( C <> {} & C is open & Cl A c= C & Cl C c= B )
( C <> {} & Cl A c= C & Cl C c= B )

proof

consider x being set such that
A10: x in W by A5, XBOOLE_0:def 1;
A11: Q ` is closed by A9;
consider Q0, C0 being Subset of ([#] T) such that
A12: ( Q0 = Q & C0 = C ) ;
C0 c= Q0 ` by A9, A12, SUBSET_1:43;
then Cl C c= Q ` by A11, A12, TOPS_1:31;
then Cl C misses Q by SUBSET_1:43;
then A13: V misses Cl C by A9, XBOOLE_1:63;
(B ` ) ` = B ;
hence ( C <> {} & Cl A c= C & Cl C c= B ) by A9, A10, A13, SUBSET_1:43; :: thesis: verum

end;

hence ex C being Subset of T st
( C <> {} & C is open & Cl A c= C & Cl C c= B ) by A9; :: thesis: verum

end;

case A14: B = [#] T ; :: thesis: ex C, C being Subset of T st
( C <> {} & C is open & Cl A c= C & Cl C c= B )

consider C being Subset of T such that
A15: C = [#] T ;
take C = C; :: thesis: ex C being Subset of T st
( C <> {} & C is open & Cl A c= C & Cl C c= B )
( C <> {} & C is open & Cl A c= C & Cl C c= B ) by A14, A15;
hence ex C being Subset of T st
( C <> {} & C is open & Cl A c= C & Cl C c= B ) ; :: thesis: verum

end;

end;

end;

hence ex C being Subset of T st
( C <> {} & C is open & Cl A c= C & Cl C c= B ) ; :: thesis: verum