let r be real number ; :: thesis: for M being non empty Reflexive symmetric triangle MetrStruct
for z being Point of M st r < 0 holds
cl_Ball z,r = {}
let M be non empty Reflexive symmetric triangle MetrStruct ; :: thesis: for z being Point of M st r < 0 holds
cl_Ball z,r = {}
let z be Point of M; :: thesis: ( r < 0 implies cl_Ball z,r = {} )
A1: (Sphere z,r) \/ (Ball z,r) = cl_Ball z,r by METRIC_1:17;
assume A2: r < 0 ; :: thesis: cl_Ball z,r = {}
then Ball z,r = {} by TBSP_1:17;
hence cl_Ball z,r = {} by A2, A1, Th61; :: thesis: verum