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 )
A1: {p} /\ ([#] T) = {p} by XBOOLE_1:28;
hereby :: thesis: ( {p} is open implies p is isolated )
assume p is isolated ; :: thesis: {p} is open
then p is_isolated_in [#] T ;
then ex G being open Subset of T st G /\ ([#] T) = {p} by Th22;
hence {p} is open ; :: thesis: verum
end;
assume {p} is open ; :: thesis: p is isolated
then p is_isolated_in [#] T by A1, Th22;
hence p is isolated ; :: thesis: verum