let r be Real; :: 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:16;
assume A2: r < 0 ; :: thesis: cl_Ball (z,r) = {}
then Ball (z,r) = {} by TBSP_1:12;
hence cl_Ball (z,r) = {} by A2, A1, Th51; :: thesis: verum