let n be Element of NAT ; :: thesis: for r being real number
for x being Point of (TOP-REAL n) holds Ball (x,r) misses Sphere (x,r)
let r be real number ; :: thesis: for x being Point of (TOP-REAL n) holds Ball (x,r) misses Sphere (x,r)
let x be Point of (TOP-REAL n); :: thesis: Ball (x,r) misses Sphere (x,r)
assume not Ball (x,r) misses Sphere (x,r) ; :: thesis: contradiction
then consider q being set such that
A1: q in Ball (x,r) and
A2: q in Sphere (x,r) by XBOOLE_0:3;
reconsider q = q as Point of (TOP-REAL n) by A1;
|.(q - x).| = r by A2, Th9;
hence contradiction by A1, Th7; :: thesis: verum