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