let n be Nat; :: thesis: for r being Real
for x being Point of (TOP-REAL n) holds Ball (x,r) misses Sphere (x,r)
let r be Real; :: 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 object 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, Th7;
hence contradiction by A1, Th5; :: thesis: verum