let n be Nat; :: thesis: for r being real number
for a, o being Point of (Euclid n) st a in Ball (o,r) holds
for x being set holds
( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r )
let r be real number ; :: thesis: for a, o being Point of (Euclid n) st a in Ball (o,r) holds
for x being set holds
( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r )
let a, o be Point of (Euclid n); :: thesis: ( a in Ball (o,r) implies for x being set holds
( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r ) )
reconsider a1 = a, o1 = o as Point of (TOP-REAL n) by EUCLID:71;
n in NAT by ORDINAL1:def 13;
then A1: Ball (o,r) = Ball (o1,r) by TOPREAL9:13;
a - o = a1 - o1 by EUCLID:73;
hence ( a in Ball (o,r) implies for x being set holds
( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r ) ) by A1, Th9; :: thesis: verum