let T be non empty TopStruct ; :: thesis: for A being Subset of T
for p being Point of T st ex K being Basis of p st
for Q being Subset of T st Q in K holds
A meets Q holds
p in Cl A
let A be Subset of T; :: thesis: for p being Point of T st ex K being Basis of p st
for Q being Subset of T st Q in K holds
A meets Q holds
p in Cl A
let p be Point of T; :: thesis: ( ex K being Basis of p st
for Q being Subset of T st Q in K holds
A meets Q implies p in Cl A )
given K being Basis of p such that A1: for Q being Subset of T st Q in K holds
A meets Q ; :: thesis: p in Cl A
assume not p in Cl A ; :: thesis: contradiction
then consider F being Subset of T such that
A2: ( F is closed & A c= F & not p in F ) by PRE_TOPC:45;
A3: p in F ` by A2, XBOOLE_0:def 5;
F ` is open by A2, TOPS_1:29;
then consider W being Subset of T such that
A4: ( W in K & W c= F ` ) by A3, YELLOW_8:22;
A5: A meets W by A1, A4;
A misses F ` by A2, SUBSET_1:44;
hence contradiction by A4, A5, XBOOLE_1:63; :: thesis: verum