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

for p being Element of M holds (Sphere (p,r)) \/ (Ball (p,r)) = cl_Ball (p,r)

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

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

( Sphere (p,r) c= cl_Ball (p,r) & Ball (p,r) c= cl_Ball (p,r) ) by Th14, Th15;

hence (Sphere (p,r)) \/ (Ball (p,r)) c= cl_Ball (p,r) by XBOOLE_1:8; :: according to XBOOLE_0:def 10 :: thesis: cl_Ball (p,r) c= (Sphere (p,r)) \/ (Ball (p,r))

for p being Element of M holds (Sphere (p,r)) \/ (Ball (p,r)) = cl_Ball (p,r)

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

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

( Sphere (p,r) c= cl_Ball (p,r) & Ball (p,r) c= cl_Ball (p,r) ) by Th14, Th15;

hence (Sphere (p,r)) \/ (Ball (p,r)) c= cl_Ball (p,r) by XBOOLE_1:8; :: according to XBOOLE_0:def 10 :: thesis: cl_Ball (p,r) c= (Sphere (p,r)) \/ (Ball (p,r))

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

end;

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

end;

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

x in (Sphere (p,r)) \/ (Ball (p,r))

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

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

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

then A2: dist (p,x) <= r by Th12;

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

then A2: dist (p,x) <= r by Th12;

now :: thesis: ( ( dist (p,x) < r & x in Ball (p,r) ) or ( dist (p,x) = r & x in Sphere (p,r) ) )

hence
x in (Sphere (p,r)) \/ (Ball (p,r))
by XBOOLE_0:def 3; :: thesis: verumend;