let T be discrete TopSpace; :: thesis: for A being Subset of T holds Der A = {}
let A be Subset of T; :: 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 object such that
A2: x in Der A by XBOOLE_0:def 1;
x is_an_accumulation_point_of A by A1, A2, Th16;
then x in Cl (A \ {x}) ;
then x in A \ {x} by PRE_TOPC:22;
hence contradiction by ZFMISC_1:56; :: thesis: verum

end;

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

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

end;

end;