A1: the carrier of (Tcircle p,r) = Sphere p,r by TOPREALB:9;
A2: the carrier of (Tdisk p,r) = cl_Ball p,r by BROUWER:3;
A3: Sphere p,r c= cl_Ball p,r by TOPREAL9:17;
consider a being Point of (Tcircle p,r);
A4: a in Sphere p,r by A1;

per cases ( a = q or a <> q ) ;

suppose A5: a = q ; :: thesis: not (cl_Ball p,r) \ {q} is empty

A6: p is Point of (Tdisk p,r) by Th17;
|.(p - p).| <> r by TOPRNS_1:29;
then p <> q by A1, A5, TOPREAL9:9;
hence not (cl_Ball p,r) \ {q} is empty by A2, A6, ZFMISC_1:64; :: thesis: verum

end;

suppose a <> q ; :: thesis: not (cl_Ball p,r) \ {q} is empty

hence not (cl_Ball p,r) \ {q} is empty by A3, A4, ZFMISC_1:64; :: thesis: verum

end;

end;