n in NAT by ORDINAL1:def 12;
hence cl_Ball (x,r) is convex by Lm1; :: thesis: verum