reconsider e = x as Point of (Euclid n) by TOPREAL3:8;
Ball (e,r) = Ball (x,r) by Th11;
hence Ball (x,r) is open by GOBOARD6:3; :: thesis: verum