let n be Nat; for r being Real
for x being Point of (TOP-REAL n) holds Ball (x,r) misses Sphere (x,r)
let r be Real; for x being Point of (TOP-REAL n) holds Ball (x,r) misses Sphere (x,r)
let x be Point of (TOP-REAL n); Ball (x,r) misses Sphere (x,r)
assume
not Ball (x,r) misses Sphere (x,r)
; 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; verum