let n be Element of NAT ; :: thesis: for x being Point of (TOP-REAL n)
for r being non zero real number holds Fr (Ball x,r) = Sphere x,r
let x be Point of (TOP-REAL n); :: thesis: for r being non zero real number holds Fr (Ball x,r) = Sphere x,r
let r be non zero real number ; :: thesis: Fr (Ball x,r) = Sphere x,r
set P = Ball x,r;
thus Fr (Ball x,r) = (Cl (Ball x,r)) \ (Ball x,r) by TOPS_1:76
.= (cl_Ball x,r) \ (Ball x,r) by Th23
.= Sphere x,r by Th19 ; :: thesis: verum