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 )

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

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

hence
for U being Subset of T
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 )

( p in O & Cl O c= U & O in Union Bn ) ; :: thesis: verum

end;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 )end;

hence
ex 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 )
;

end;

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 )

( 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;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

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 )

( 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;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

( p in O & Cl O c= U & O in Union Bn ) ; :: thesis: verum

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