let r be Real; :: thesis: for n being non zero Nat
for p being Element of (EMINFTY n) holds Ball (p,r) = OpenHyperInterval (((@ p) - (n |-> r)),((@ p) + (n |-> r)))
let n be non zero Nat; :: thesis: for p being Element of (EMINFTY n) holds Ball (p,r) = OpenHyperInterval (((@ p) - (n |-> r)),((@ p) + (n |-> r)))
let p be Element of (EMINFTY n); :: thesis: Ball (p,r) = OpenHyperInterval (((@ p) - (n |-> r)),((@ p) + (n |-> r)))
reconsider e = p as Point of (Euclid n) ;
ex a being Element of REAL n st
( a = e & OpenHypercube (e,r) = OpenHyperInterval ((a - (n |-> r)),(a + (n |-> r))) ) by Th51;
hence Ball (p,r) = OpenHyperInterval (((@ p) - (n |-> r)),((@ p) + (n |-> r))) by Th68; :: thesis: verum