let T be non empty TopSpace; :: thesis: for A being Subset of T
for p being Point of T holds
( p is_isolated_in A iff ex G being open Subset of T st G /\ A = {p} )
let A be Subset of T; :: thesis: for p being Point of T holds
( p is_isolated_in A iff ex G being open Subset of T st G /\ A = {p} )
let p be Point of T; :: thesis: ( p is_isolated_in A iff ex G being open Subset of T st G /\ A = {p} )

hereby :: thesis: ( ex G being open Subset of T st G /\ A = {p} implies p is_isolated_in A )

assume A1: p is_isolated_in A ; :: thesis: ex U being open Subset of T st U /\ A = {p}
then not p is_an_accumulation_point_of A ;
then consider U being open Subset of T such that
A2: p in U and
A3: for q being Point of T holds
( not q <> p or not q in A or not q in U ) by Th21;
take U = U; :: thesis: U /\ A = {p}
A4: p in A by A1;
U /\ A = {p}

proof

thus U /\ A c= {p} :: according to XBOOLE_0:def 10 :: thesis: {p} c= U /\ A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in U /\ A or x in {p} )
assume x in U /\ A ; :: thesis: x in {p}
then ( x in U & x in A ) by XBOOLE_0:def 4;
then x = p by A3;
hence x in {p} by TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {p} or x in U /\ A )
assume x in {p} ; :: thesis: x in U /\ A
then x = p by TARSKI:def 1;
hence x in U /\ A by A4, A2, XBOOLE_0:def 4; :: thesis: verum

end;

hence U /\ A = {p} ; :: thesis: verum

end;

given G being open Subset of T such that A5: G /\ A = {p} ; :: thesis: p is_isolated_in A
A6: p in G /\ A by A5, TARSKI:def 1;
ex U being open Subset of T st
( p in U & ( for q being Point of T holds
( not q <> p or not q in A or not q in U ) ) )

proof

take G ; :: thesis: ( p in G & ( for q being Point of T holds
( not q <> p or not q in A or not q in G ) ) )
for q being Point of T holds
( q = p or not q in A or not q in G )

proof

given q being Point of T such that A7: q <> p and
A8: ( q in A & q in G ) ; :: thesis: contradiction
q in A /\ G by A8, XBOOLE_0:def 4;
hence contradiction by A5, A7, TARSKI:def 1; :: thesis: verum

end;

hence ( p in G & ( for q being Point of T holds
( not q <> p or not q in A or not q in G ) ) ) by A6, XBOOLE_0:def 4; :: thesis: verum

end;

then A9: not p is_an_accumulation_point_of A by Th21;
p in A by A6, XBOOLE_0:def 4;
hence p is_isolated_in A by A9; :: thesis: verum