let T be non empty TopSpace; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 A3: ( U is open & p in U ) ; :: thesis: ex O being Subset of T st
( p in O & Cl O c= U & O in Union Bn )

now

per cases ( U = the carrier of T or U <> the carrier of T ) ;

suppose A4: U = the carrier of T ; :: thesis: ex O, O being Subset of T st
( p in O & Cl O c= U & O in Union Bn )

consider O being Subset of T such that
A5: ( O in Union Bn & p in O & O c= U ) by A2, A3, YELLOW_9:31;
take O = O; :: thesis: ex O being Subset of T st
( p in O & Cl O c= U & O in Union Bn )
( p in O & Cl O c= U & O in Union Bn ) by A4, A5;
hence ex O being Subset of T st
( p in O & Cl O c= U & O in Union Bn ) ; :: thesis: verum

end;

suppose U <> the carrier of T ; :: thesis: 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 ( U ` <> {} & p in (U ` ) ` & U ` is closed ) by A3, XBOOLE_1:105;
then consider W, V being Subset of T such that
A6: ( W is open & V is open & p in W & U ` c= V & W misses V ) by A1, COMPTS_1:def 5;
A7: ( W c= V ` & V ` c= U & V ` is closed ) by A6, SUBSET_1:36, SUBSET_1:43;
consider O being Subset of T such that
A8: ( O in Union Bn & p in O & O c= W ) by A2, A6, YELLOW_9:31;
take O = O; :: thesis: ex O being Subset of T st
( p in O & Cl O c= U & O in Union Bn )
O c= V ` by A7, A8, XBOOLE_1:1;
then Cl O c= Cl (V ` ) by PRE_TOPC:49;
then Cl O c= V ` by A7, PRE_TOPC:52;
hence ex O being Subset of T st
( p in O & Cl O c= U & O in Union Bn ) by A7, A8, XBOOLE_1:1; :: thesis: verum

end;

end;

end;

hence ex O being Subset of T st
( p in O & Cl O c= U & O in Union Bn ) ; :: thesis: 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 ) ; :: thesis: verum