reconsider e = x as Point of (Euclid n) by TOPREAL3:8;
A4: n in NAT by ORDINAL1:def 12;
then ( Sphere (e,r) is bounded & Sphere (e,r) = Sphere (x,r) ) by Th15, TOPREAL6:62;
hence Sphere (x,r) is closed by A4, TOPREAL6:61; :: thesis: verum