let A be Subset of (TOP-REAL 2); :: according to BORSUK_1:def 14 :: 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