let r be Real; :: thesis: for M being non empty Reflexive symmetric triangle MetrStruct
for z being Point of M st r < 0 holds
Sphere (z,r) = {}
let M be non empty Reflexive symmetric triangle MetrStruct ; :: thesis: for z being Point of M st r < 0 holds
Sphere (z,r) = {}
let z be Point of M; :: thesis: ( r < 0 implies Sphere (z,r) = {} )
assume A1: r < 0 ; :: thesis: Sphere (z,r) = {}
thus Sphere (z,r) c= {} :: according to XBOOLE_0:def 10 :: thesis: {} c= Sphere (z,r)
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Sphere (z,r) or a in {} )
assume A2: a in Sphere (z,r) ; :: thesis: a in {}
then reconsider b = a as Point of M ;
dist (b,z) = r by A2, METRIC_1:13;
hence a in {} by A1, METRIC_1:5; :: thesis: verum
end;
thus {} c= Sphere (z,r) ; :: thesis: verum