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 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 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 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 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 and
A3: A c= F and
A4: not p in F by PRE_TOPC:15;
A5: A misses F ` by A3, SUBSET_1:24;
( p in F ` & F ` is open ) by A2, A4, XBOOLE_0:def 5;
then consider W being Subset of T such that
A6: W in K and
A7: W c= F ` by YELLOW_8:13;
A meets W by A1, A6;
hence contradiction by A7, A5, XBOOLE_1:63; :: thesis: verum