reconsider e = x as Point of (Euclid n) by TOPREAL3:13;
A1: ( r is Real & Ball e,r is bounded ) by TBSP_1:19, XREAL_0:def 1;
Ball e,r = Ball x,r by Th13;
hence Ball x,r is Bounded by A1, GOBOARD6:6, JORDAN2C:def 2; :: thesis: verum