let X be RealUnitarySpace; :: thesis: for y, x being Point of X
for r being Real st y in Ball x,r holds
y - x in Ball (0. X),r
let y, x 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 14;
then ||.(- (y - x)).|| < r by RLVECT_1:47;
then ||.(H₁(X) - (y - x)).|| < r by RLVECT_1:27;
hence y - x in Ball (0. X),r ; :: thesis: verum