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

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