let T be non empty TopStruct ; :: thesis: for A being Subset of T
for p being Point of T holds
( p in Cl A iff 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 holds
( p in Cl A iff 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 iff for K being Basis of
for Q being Subset of T st Q in K holds
A meets Q )
thus ( p in Cl A implies for K being Basis of
for Q being Subset of T st Q in K holds
A meets Q ) by Lm1; :: thesis: ( ( for K being Basis of
for Q being Subset of T st Q in K holds
A meets Q ) implies p in Cl A )
assume for K being Basis of
for Q being Subset of T st Q in K holds
A meets Q ; :: thesis: p in Cl A
then ex K being Basis of st
for Q being Subset of T st Q in K holds
A meets Q by Lm2;
hence p in Cl A by Lm3; :: thesis: verum