reconsider e = x as Point of (Euclid n) by TOPREAL3:13;
n in NAT by ORDINAL1:def 13;
then Ball (x,r) = Ball (e,r) by Th13;
hence not Ball (x,r) is empty by GOBOARD6:4; :: thesis: verum