let r be Real; :: thesis: for n being non zero Nat
for p being Element of (EMINFTY n) holds cl_Ball (p,r) = ClosedHyperInterval (((@ p) - (n |-> r)),((@ p) + (n |-> r)))
let n be non zero Nat; :: thesis: for p being Element of (EMINFTY n) holds cl_Ball (p,r) = ClosedHyperInterval (((@ p) - (n |-> r)),((@ p) + (n |-> r)))
let p be Element of (EMINFTY n); :: thesis: cl_Ball (p,r) = ClosedHyperInterval (((@ p) - (n |-> r)),((@ p) + (n |-> r)))
reconsider q = p as Point of (TOP-REAL n) by EUCLID:22;
ex a being Element of REAL n st
( a = p & ClosedHypercube (q,(n |-> r)) = ClosedHyperInterval ((a - (n |-> r)),(a + (n |-> r))) ) by Th52;
hence cl_Ball (p,r) = ClosedHyperInterval (((@ p) - (n |-> r)),((@ p) + (n |-> r))) by Th70; :: thesis: verum