let T be discrete TopSpace; :: thesis: for A being Subset of holds Der A = {}
let A be Subset of ; :: thesis: Der A = {}

per cases ( not T is empty or T is empty ) ;

suppose A1: not T is empty ; :: thesis: Der A = {}

assume Der A <> {} ; :: thesis: contradiction
then consider x being set such that
A2: x in Der A by XBOOLE_0:def 1;
x is_an_accumulation_point_of A by A1, A2, Th18;
then x in Cl (A \ {x}) by Def2;
then x in A \ {x} by PRE_TOPC:52;
hence contradiction by ZFMISC_1:64; :: thesis: verum

end;

suppose T is empty ; :: thesis: Der A = {}

then the carrier of T is empty ;
hence Der A = {} ; :: thesis: verum

end;

end;