let T be non empty TopSpace; :: thesis: for A being Subset of T
for p being set holds
( p in A \ (Der A) iff p is_isolated_in A )
let A be Subset of T; :: thesis: for p being set holds
( p in A \ (Der A) iff p is_isolated_in A )
let p be set ; :: thesis: ( p in A \ (Der A) iff p is_isolated_in A )

hereby :: thesis: ( p is_isolated_in A implies p in A \ (Der A) )

assume p in A \ (Der A) ; :: thesis: p is_isolated_in A
then A1: ( p in A & not p in Der A ) by XBOOLE_0:def 5;
then not p is_an_accumulation_point_of A by Th18;
hence p is_isolated_in A by A1, Def4; :: thesis: verum

end;

assume p is_isolated_in A ; :: thesis: p in A \ (Der A)
then A2: ( p in A & not p is_an_accumulation_point_of A ) by Def4;
then not p in Der A by Th18;
hence p in A \ (Der A) by A2, XBOOLE_0:def 5; :: thesis: verum