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 that
A1: T is normal and
A2: 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 A3: A <> {} ; :: thesis: ex B being Subset of T st
( B <> {} & Cl B c= A )

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

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

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

reconsider V = ([#] T) \ A as Subset of T ;
consider x being object such that
A4: x in A by A3, XBOOLE_0:def 1;
A = ([#] T) \ V by PRE_TOPC:3;
then A5: V is closed ;
reconsider x = x as Point of T by A4;
consider W being set such that
A6: W = {x} ;
reconsider W = W as Subset of T by A6;
A7: W misses V

proof

assume W meets V ; :: thesis: contradiction
then consider z being object such that
A8: z in W /\ V by XBOOLE_0:4;
z in W by A8, XBOOLE_0:def 4;
then A9: z in A by A4, A6, TARSKI:def 1;
z in V by A8, XBOOLE_0:def 4;
hence contradiction by A9, XBOOLE_0:def 5; :: thesis: verum

end;

W is closed by A2, A6, Th19;
then consider B, Q being Subset of T such that
B is open and
A10: Q is open and
A11: W c= B and
A12: V c= Q and
A13: B misses Q by A1, A5, A7;
take B = B; :: thesis: ex B being Subset of T st
( B <> {} & Cl B c= A )
( B <> {} & Cl B c= A )

proof

B c= Q ` by A13, SUBSET_1:23;
then Cl B c= Q ` by A10, TOPS_1:5;
then Cl B misses Q by SUBSET_1:23;
then A14: V misses Cl B by A12, XBOOLE_1:63;
(A `) ` = A ;
hence ( B <> {} & Cl B c= A ) by A6, A11, A14, SUBSET_1:23; :: thesis: verum

end;

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

end;

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

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

end;

end;

end;

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