let r be real number ; :: thesis:
let n be Element of NAT ; :: thesis:
let x be Point of (TOP-REAL n); :: thesis:
thus (cl_Ball x,r) \ (Ball x,r) c= Sphere x,r :: according to XBOOLE_0:def 10 :: thesis:

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume A1: a in (cl_Ball x,r) \ (Ball x,r) ; :: thesis:
then reconsider a = a as Point of (TOP-REAL n) ;
A2: a in cl_Ball x,r by A1, XBOOLE_0:def 5;
A3: not a in Ball x,r by A1, XBOOLE_0:def 5;
A4: |.(a - x).| <= r by A2, TOPREAL9:8;
|.(a - x).| >= r by A3, TOPREAL9:7;
then |.(a - x).| = r by A4, XXREAL_0:1;
hence a in Sphere x,r by TOPREAL9:9; :: thesis:

end;

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume A5: a in Sphere x,r ; :: thesis:
then reconsider a = a as Point of (TOP-REAL n) ;
A6: |.(a - x).| = r by A5, TOPREAL9:9;
then A7: a in cl_Ball x,r by TOPREAL9:8;
not a in Ball x,r by A6, TOPREAL9:7;
hence a in (cl_Ball x,r) \ (Ball x,r) by A7, XBOOLE_0:def 5; :: thesis: