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 ex B being Basis of x st
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 ex B being Basis of x st
for U being set st U in B holds
U meets A )
let x be Element of T; :: thesis: ( x in Cl A iff ex B being Basis of x st
for U being set st U in B holds
U meets A )
set B = the Basis of x;
( x in Cl A implies for U being set st U in the Basis of x holds
U meets A ) by Lm2;
hence ( x in Cl A implies ex B being Basis of x st
for U being set st U in B holds
U meets A ) ; :: thesis: ( ex B being Basis of x st
for U being set st U in B holds
U meets A implies x in Cl A )
thus ( ex B being Basis of x st
for U being set st U in B holds
U meets A implies x in Cl A ) by Lm3; :: thesis: verum