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