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 A1: p in A \ (Der A) ; :: thesis: p is_isolated_in A
then not p in Der A by XBOOLE_0:def 5;
then A2: not p is_an_accumulation_point_of A by Th16;
p in A by A1, XBOOLE_0:def 5;
hence p is_isolated_in A by A2; :: thesis: verum

end;

assume A3: p is_isolated_in A ; :: thesis: p in A \ (Der A)
then not p is_an_accumulation_point_of A ;
then A4: not p in Der A by Th16;
p in A by A3;
hence p in A \ (Der A) by A4, XBOOLE_0:def 5; :: thesis: verum