let n be Element of NAT ; :: thesis: for x being Point of (TOP-REAL n)
for r being non zero Real holds Fr (Ball (x,r)) = Sphere (x,r)
let x be Point of (TOP-REAL n); :: thesis: for r being non zero Real holds Fr (Ball (x,r)) = Sphere (x,r)
let r be non zero Real; :: 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:42
.= (cl_Ball (x,r)) \ (Ball (x,r)) by Th23
.= Sphere (x,r) by Th19 ; :: thesis: verum