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, TOPS_1:51;
then A meets Int G by A1, PRE_TOPC:def 13;
hence G meets A by TOPS_1:44, 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

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 Th5;
hence A meets G by A2; :: thesis: verum

end;

hence p in Cl A by PRE_TOPC:def 13; :: thesis: verum