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

now

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

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

consider x being set such that
A4: x in A by A2, XBOOLE_0:def 1;
reconsider x = x as Point of T by A4;
consider W being set such that
A5: W = {x} ;
reconsider W = W as Subset of T by A5;
A6: W is closed by A1, A5, Th27;
reconsider V = ([#] T) \ A as Subset of T ;
A = ([#] T) \ V by PRE_TOPC:22;
then A7: V is closed by PRE_TOPC:def 6;
A8: ([#] T) \ A <> {}

proof

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

end;

W misses V

proof

assume W meets V ; :: thesis: contradiction
then consider z being set such that
A9: z in W /\ V by XBOOLE_0:4;
( z in W & z in V ) by A9, XBOOLE_0:def 4;
then ( z in A & not z in A ) by A4, A5, TARSKI:def 1, XBOOLE_0:def 5;
hence contradiction ; :: thesis: verum

end;

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

proof

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

end;

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

end;

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

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

end;

end;

end;

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