reconsider e = x as Point of (Euclid n) by TOPREAL3:13;
A3: cl_Ball e,r is bounded by TOPREAL6:67;
cl_Ball e,r = cl_Ball x,r by Th14;
hence ( cl_Ball x,r is closed & cl_Ball x,r is Bounded ) by A3, JORDAN2C:def 2, TOPREAL6:66; :: thesis: verum