let T be non empty TopSpace; :: thesis: for p being Point of T holds
( p is isolated iff {p} is open )
let p be Point of T; :: thesis: ( p is isolated iff {p} is open )

hereby :: thesis: ( {p} is open implies p is isolated )

assume p is isolated ; :: thesis: {p} is open
then p is_isolated_in [#] T by Def5;
then consider G being open Subset of T such that
A1: G /\ ([#] T) = {p} by Th24;
thus {p} is open by A1, XBOOLE_1:28; :: thesis: verum

end;

assume A2: {p} is open ; :: thesis: p is isolated
{p} /\ ([#] T) = {p} by XBOOLE_1:28;
then p is_isolated_in [#] T by A2, Th24;
hence p is isolated by Def5; :: thesis: verum