let T be non empty TopStruct ; :: thesis: for A being Subset of
for p being Point of holds
( p in Cl A iff ex K being Basis of st
for Q being Subset of st Q in K holds
A meets Q )
let A be Subset of ; :: thesis: for p being Point of holds
( p in Cl A iff ex K being Basis of st
for Q being Subset of st Q in K holds
A meets Q )
let p be Point of ; :: thesis: ( p in Cl A iff ex K being Basis of st
for Q being Subset of st Q in K holds
A meets Q )

hereby :: thesis: ( ex K being Basis of st
for Q being Subset of st Q in K holds
A meets Q implies p in Cl A )

assume p in Cl A ; :: thesis: ex K being Basis of st
for Q being Subset of st Q in K holds
A meets Q
then for K being Basis of
for Q being Subset of st Q in K holds
A meets Q by Lm1;
hence ex K being Basis of st
for Q being Subset of st Q in K holds
A meets Q by Lm2; :: thesis: verum

end;

assume ex K being Basis of st
for Q being Subset of st Q in K holds
A meets Q ; :: thesis: p in Cl A
hence p in Cl A by Lm3; :: thesis: verum