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 )

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 A2:
for G being a_neighborhood of p holds G meets A
; :: thesis: p in Cl Aassume 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;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

now :: thesis: for G being Subset of T st G is open & p in G holds

A meets G

hence
p in Cl A
by PRE_TOPC:def 7; :: thesis: verumA 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;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