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;
set a = the Point of (Tcircle (p,r));
A4: the Point of (Tcircle (p,r)) in Sphere (p,r) by A1;

per cases ( the Point of (Tcircle (p,r)) = q or the Point of (Tcircle (p,r)) <> q ) ;

suppose A5: the Point of (Tcircle (p,r)) = 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:28;
then p <> q by A1, A5, TOPREAL9:9;
hence not (cl_Ball (p,r)) \ {q} is empty by A2, A6, ZFMISC_1:56; :: thesis: verum

end;

suppose the Point of (Tcircle (p,r)) <> q ; :: thesis: not (cl_Ball (p,r)) \ {q} is empty

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

end;

end;