let A be Subset of (TOP-REAL 2); :: according to BORSUK_1:def 11 :: thesis: ( not A = the carrier of (Tdisk (p,r)) or A is closed )
assume A = the carrier of (Tdisk (p,r)) ; :: thesis: A is closed
then A = cl_Ball (p,r) by BROUWER:3;
hence A is closed ; :: thesis: verum