set D = Tdisk p,r;
reconsider Q = [#] (Tdisk p,r) as Subset of (TOP-REAL 2) by TSEP_1:1;
[#] (Tdisk p,r) = cl_Ball p,r by BROUWER:3;
then Q is compact by TOPREAL6:88;
then [#] (Tdisk p,r) is compact by COMPTS_1:11;
hence Tdisk p,r is compact by COMPTS_1:10; :: thesis: verum