let T be non empty TopSpace; ( T is regular implies for Bn being FamilySequence of T st Union Bn is Basis of T holds
for U being Subset of T
for p being Point of T st U is open & p in U holds
ex O being Subset of T st
( p in O & Cl O c= U & O in Union Bn ) )
assume A1:
T is regular
; for Bn being FamilySequence of T st Union Bn is Basis of T holds
for U being Subset of T
for p being Point of T st U is open & p in U holds
ex O being Subset of T st
( p in O & Cl O c= U & O in Union Bn )
let Bn be FamilySequence of T; ( Union Bn is Basis of T implies for U being Subset of T
for p being Point of T st U is open & p in U holds
ex O being Subset of T st
( p in O & Cl O c= U & O in Union Bn ) )
assume A2:
Union Bn is Basis of T
; for U being Subset of T
for p being Point of T st U is open & p in U holds
ex O being Subset of T st
( p in O & Cl O c= U & O in Union Bn )
for U being open Subset of T
for p being Point of T st U is open & p in U holds
ex O being Subset of T st
( p in O & Cl O c= U & O in Union Bn )
proof
let U be
open Subset of
T;
for p being Point of T st U is open & p in U holds
ex O being Subset of T st
( p in O & Cl O c= U & O in Union Bn )let p be
Point of
T;
( U is open & p in U implies ex O being Subset of T st
( p in O & Cl O c= U & O in Union Bn ) )
assume that
U is
open
and A3:
p in U
;
ex O being Subset of T st
( p in O & Cl O c= U & O in Union Bn )
now ex O, O being Subset of T st
( p in O & Cl O c= U & O in Union Bn )per cases
( U = the carrier of T or U <> the carrier of T )
;
suppose
U <> the
carrier of
T
;
ex O, O being Subset of T st
( p in O & Cl O c= U & O in Union Bn )then
U c< the
carrier of
T
by XBOOLE_0:def 8;
then A6:
U ` <> {}
by XBOOLE_1:105;
p in (U `) `
by A3;
then consider W,
V being
Subset of
T such that A7:
W is
open
and A8:
V is
open
and A9:
p in W
and A10:
U ` c= V
and A11:
W misses V
by A1, A6;
consider O being
Subset of
T such that A12:
(
O in Union Bn &
p in O )
and A13:
O c= W
by A2, A7, A9, YELLOW_9:31;
W c= V `
by A11, SUBSET_1:23;
then
O c= V `
by A13;
then
Cl O c= Cl (V `)
by PRE_TOPC:19;
then A14:
Cl O c= V `
by A8, PRE_TOPC:22;
take O =
O;
ex O being Subset of T st
( p in O & Cl O c= U & O in Union Bn )
V ` c= U
by A10, SUBSET_1:17;
hence
ex
O being
Subset of
T st
(
p in O &
Cl O c= U &
O in Union Bn )
by A12, A14, XBOOLE_1:1;
verum end;
hence
ex
O being
Subset of
T st
(
p in O &
Cl O c= U &
O in Union Bn )
;
verum
end;
hence
for U being Subset of T
for p being Point of T st U is open & p in U holds
ex O being Subset of T st
( p in O & Cl O c= U & O in Union Bn )
; verum