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:79;
then [#] (Tdisk (p,r)) is compact by COMPTS_1:2;
hence Tdisk (p,r) is compact by COMPTS_1:1; :: thesis: verum