reconsider e = x as Point of (Euclid n) by TOPREAL3:13;
A1: n in NAT by ORDINAL1:def 13;
then ( cl_Ball e,r is bounded & cl_Ball e,r = cl_Ball x,r ) by Th14, TOPREAL6:67;
hence cl_Ball x,r is closed by A1, TOPREAL6:66; :: thesis: verum