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
per cases ( A <> [#] T or A = [#] T ) ;
case A4: A <> [#] T ; :: thesis: ex B, B being Subset of T st
( B <> {} & Cl B c= A )
A5: ([#] T) \ A <> {}
proof
assume ([#] T) \ A = {} ; :: thesis: contradiction
then A = ([#] T) \ {} by PRE_TOPC:22;
hence contradiction by A4; :: thesis: verum
end;
reconsider V = ([#] T) \ A as Subset of T ;
consider x being set such that
A6: x in A by A3, XBOOLE_0:def 1;
A = ([#] T) \ V by PRE_TOPC:22;
then A7: V is closed by PRE_TOPC:def 6;
reconsider x = x as Point of T by A6;
consider W being set such that
A8: W = {x} ;
reconsider W = W as Subset of T by A8;
A9: W misses V
proof
assume W meets V ; :: thesis: contradiction
then consider z being set such that
A10: z in W /\ V by XBOOLE_0:4;
z in W by A10, XBOOLE_0:def 4;
then A11: z in A by A6, A8, TARSKI:def 1;
z in V by A10, XBOOLE_0:def 4;
hence contradiction by A11, XBOOLE_0:def 5; :: thesis: verum
end;
W is closed by A2, A8, Th27;
then consider B, Q being Subset of T such that
B is open and
A12: Q is open and
A13: W c= B and
A14: V c= Q and
A15: B misses Q by A1, A8, A7, A5, A9, 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 ) hence ex B being Subset of T st
( B <> {} & Cl B c= A ) ; :: thesis: verum
end;
case A17: A = [#] T ; :: thesis: ex B, B being Subset of T st
( B <> {} & Cl B c= A )
consider B being Subset of T such that
A18: B = [#] T ;
take B = B; :: thesis: ex B being Subset of T st
( B <> {} & Cl B c= A )
Cl B c= A by A17;
hence ex B being Subset of T st
( B <> {} & Cl B c= A ) by A18; :: thesis: verum
end;
end;
end;
hence ex B being Subset of T st
( B <> {} & Cl B c= A ) ; :: thesis: verum