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 ;
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 ;
W c= V ` by ;
then O c= V ` by A13;
then Cl O c= Cl (V `) by PRE_TOPC:19;
then A14: Cl O c= V ` by ;
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 ;
hence ex O being Subset of T st
( p in O & Cl O c= U & O in Union Bn ) by ; :: 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