let T be non empty TopSpace; :: thesis:
assume A1: T is normal ; :: thesis:
let A, B be open Subset of T; :: thesis:
assume that
A2: A <> {} and
A3: Cl A c= B ; :: thesis:

now :: thesis:

per cases ;

case A4: B <> [#] T ; :: thesis:

reconsider W = Cl A, V = ([#] T) \ B as Subset of T ;
A5: ( W <> {} & V <> {} )

proof

A6: ([#] T) \ B <> {}

proof

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

end;

A c= Cl A by PRE_TOPC:18;
hence ( W <> {} & V <> {} ) by A2, A6; :: thesis:

end;

A7: W misses V

proof

assume W meets V ; :: thesis:
then consider x being object 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 A3, XBOOLE_0:def 5; :: thesis:

end;

B = ([#] T) \ V by PRE_TOPC:3;
then V is closed ;
then consider C, Q being Subset of T such that
A9: C is open and
A10: Q is open and
A11: W c= C and
A12: V c= Q and
A13: C misses Q by A1, A7;
take C = C; :: thesis:
( C <> {} & Cl A c= C & Cl C c= B )

proof

consider Q0, C0 being Subset of ([#] T) such that
A14: ( Q0 = Q & C0 = C ) ;
C0 c= Q0 ` by A13, A14, SUBSET_1:23;
then Cl C c= Q ` by A10, A14, TOPS_1:5;
then Cl C misses Q by SUBSET_1:23;
then A15: V misses Cl C by A12, XBOOLE_1:63;
(B `) ` = B ;
hence ( C <> {} & Cl A c= C & Cl C c= B ) by A5, A11, A15, SUBSET_1:23; :: thesis:

end;

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

end;

case A16: B = [#] T ; :: thesis:

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

end;

end;

end;

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