let r be Real; :: thesis: for M being MetrStruct

for p being Element of M holds Sphere (p,r) c= cl_Ball (p,r)

let M be MetrStruct ; :: thesis: for p being Element of M holds Sphere (p,r) c= cl_Ball (p,r)

let p be Element of M; :: thesis: Sphere (p,r) c= cl_Ball (p,r)

for p being Element of M holds Sphere (p,r) c= cl_Ball (p,r)

let M be MetrStruct ; :: thesis: for p being Element of M holds Sphere (p,r) c= cl_Ball (p,r)

let p be Element of M; :: thesis: Sphere (p,r) c= cl_Ball (p,r)

per cases
( not M is empty or M is empty )
;

end;

suppose A1:
not M is empty
; :: thesis: Sphere (p,r) c= cl_Ball (p,r)

end;

now :: thesis: for x being Element of M st x in Sphere (p,r) holds

x in cl_Ball (p,r)

hence
Sphere (p,r) c= cl_Ball (p,r)
by SUBSET_1:2; :: thesis: verumx in cl_Ball (p,r)

let x be Element of M; :: thesis: ( x in Sphere (p,r) implies x in cl_Ball (p,r) )

assume x in Sphere (p,r) ; :: thesis: x in cl_Ball (p,r)

then dist (p,x) = r by Th13;

then x in { q where q is Element of M : dist (p,q) <= r } ;

hence x in cl_Ball (p,r) by Def15, A1; :: thesis: verum

end;assume x in Sphere (p,r) ; :: thesis: x in cl_Ball (p,r)

then dist (p,x) = r by Th13;

then x in { q where q is Element of M : dist (p,q) <= r } ;

hence x in cl_Ball (p,r) by Def15, A1; :: thesis: verum