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 )

( B <> {} & Cl B c= A ) ; :: thesis: verum

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 ) ) )end;

hence
ex 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 )
;

end;

case
A <> [#] T
; :: thesis: ex B, B being Subset of T st

( B <> {} & Cl B c= A )

( 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

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 )

( B <> {} & Cl B c= A ) ; :: thesis: verum

end;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

W is closed
by A2, A6, Th19;
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;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

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

hence
ex B being Subset of T st
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;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

( B <> {} & Cl B c= A ) ; :: thesis: verum

case A15:
A = [#] T
; :: thesis: ex B, B being Subset of T st

( B <> {} & Cl B c= A )

( 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;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

( B <> {} & Cl B c= A ) ; :: thesis: verum