reconsider e = x as Point of (Euclid n) by TOPREAL3:8;
A3: n in NAT by ORDINAL1:def 12;
then ( cl_Ball (e,r) is bounded & cl_Ball (e,r) = cl_Ball (x,r) ) by Th14, TOPREAL6:59;
hence cl_Ball (x,r) is closed by A3, TOPREAL6:58; :: thesis: verum