let T be non empty TopStruct ; :: thesis: for A being Subset of T
for p being Point of T st p in Cl A holds
for K being Basis of
for Q being Subset of T st Q in K holds
A meets Q
let A be Subset of T; :: thesis: for p being Point of T st p in Cl A holds
for K being Basis of
for Q being Subset of T st Q in K holds
A meets Q
let p be Point of T; :: thesis: ( p in Cl A implies for K being Basis of
for Q being Subset of T st Q in K holds
A meets Q )
assume A1: p in Cl A ; :: thesis: for K being Basis of
for Q being Subset of T st Q in K holds
A meets Q
let K be Basis of ; :: thesis: for Q being Subset of T st Q in K holds
A meets Q
let Q be Subset of T; :: thesis: ( Q in K implies A meets Q )
assume Q in K ; :: thesis: A meets Q
then ( Q is open & p in Q ) by YELLOW_8:12;
then A meets Q by A1, PRE_TOPC:def 7;
hence A /\ Q <> {} ; :: according to XBOOLE_0:def 7 :: thesis: verum