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;