let X be RealUnitarySpace; :: thesis: for x, y being Point of X
for r being Real st y in Ball (x,r) holds
y - x in Ball ((0. X),r)
let x, y be Point of X; :: thesis: for r being Real st y in Ball (x,r) holds
y - x in Ball ((0. X),r)
let r be Real; :: thesis: ( y in Ball (x,r) implies y - x in Ball ((0. X),r) )
assume y in Ball (x,r) ; :: thesis: y - x in Ball ((0. X),r)
then ||.(x - y).|| < r by Th40;
then ||.((- y) + x).|| < r by RLVECT_1:def 11;
then ||.(- (y - x)).|| < r by RLVECT_1:33;
then ||.(H₁(X) - (y - x)).|| < r by RLVECT_1:14;
hence y - x in Ball ((0. X),r) ; :: thesis: verum