let T be non empty TopSpace; :: thesis: for A being Subset of T
for x being Element of T holds
( x in Cl A iff for B being Basis of x
for U being set st U in B holds
U meets A )
let A be Subset of T; :: thesis: for x being Element of T holds
( x in Cl A iff for B being Basis of x
for U being set st U in B holds
U meets A )
let x be Element of T; :: thesis: ( x in Cl A iff for B being Basis of x
for U being set st U in B holds
U meets A )
set B = the Basis of x;
thus ( x in Cl A implies for B being Basis of x
for U being set st U in B holds
U meets A ) by Lm2; :: thesis: ( ( for B being Basis of x
for U being set st U in B holds
U meets A ) implies x in Cl A )
assume for B being Basis of x
for U being set st U in B holds
U meets A ; :: thesis: x in Cl A
then for U being set st U in the Basis of x holds
U meets A ;
hence x in Cl A by Lm3; :: thesis: verum