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 ex K being Basis of st
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 ex K being Basis of st
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 ex K being Basis of st
for Q being Subset of T st Q in K holds
A meets Q )

hereby :: 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 )

assume p in Cl A ; :: thesis: ex K being Basis of st
for Q being Subset of T st Q in K holds
A meets Q
then for K being Basis of
for Q being Subset of T st Q in K holds
A meets Q by Lm1;
hence ex K being Basis of st
for Q being Subset of T 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 T st Q in K holds
A meets Q ; :: thesis: p in Cl A
hence p in Cl A by Lm3; :: thesis: verum