let T be non empty TopSpace; :: thesis: for A being Subset of T
for p being Point of T holds
( p in Cl A iff for G being a_neighborhood of p holds G meets A )
let A be Subset of T; :: thesis: for p being Point of T holds
( p in Cl A iff for G being a_neighborhood of p holds G meets A )
let p be Point of T; :: thesis: ( p in Cl A iff for G being a_neighborhood of p holds G meets A )
hereby :: thesis: ( ( for G being a_neighborhood of p holds G meets A ) implies p in Cl A )
assume A1: p in Cl A ; :: thesis: for G being a_neighborhood of p holds G meets A
let G be a_neighborhood of p; :: thesis: G meets A
( p in Int G & Int G is open ) by Def1;
then A meets Int G by A1, PRE_TOPC:def 7;
hence G meets A by TOPS_1:16, XBOOLE_1:63; :: thesis: verum
end;
assume A2: for G being a_neighborhood of p holds G meets A ; :: thesis: p in Cl A
now :: thesis: for G being Subset of T st G is open & p in G holds
A meets G
let G be Subset of T; :: thesis: ( G is open & p in G implies A meets G )
assume ( G is open & p in G ) ; :: thesis: A meets G
then G is a_neighborhood of p by Th3;
hence A meets G by A2; :: thesis: verum
end;
hence p in Cl A by PRE_TOPC:def 7; :: thesis: verum