let r be Real; for n being Element of NAT
for x being Point of (TOP-REAL n) holds (cl_Ball (x,r)) \ (Ball (x,r)) = Sphere (x,r)
let n be Element of NAT ; for x being Point of (TOP-REAL n) holds (cl_Ball (x,r)) \ (Ball (x,r)) = Sphere (x,r)
let x be Point of (TOP-REAL n); (cl_Ball (x,r)) \ (Ball (x,r)) = Sphere (x,r)
thus
(cl_Ball (x,r)) \ (Ball (x,r)) c= Sphere (x,r)
XBOOLE_0:def 10 Sphere (x,r) c= (cl_Ball (x,r)) \ (Ball (x,r))proof
let a be
object ;
TARSKI:def 3 ( not a in (cl_Ball (x,r)) \ (Ball (x,r)) or a in Sphere (x,r) )
assume A1:
a in (cl_Ball (x,r)) \ (Ball (x,r))
;
a in Sphere (x,r)
then reconsider a =
a as
Point of
(TOP-REAL n) ;
A2:
a in cl_Ball (
x,
r)
by A1, XBOOLE_0:def 5;
A3:
not
a in Ball (
x,
r)
by A1, XBOOLE_0:def 5;
A4:
|.(a - x).| <= r
by A2, TOPREAL9:8;
|.(a - x).| >= r
by A3, TOPREAL9:7;
then
|.(a - x).| = r
by A4, XXREAL_0:1;
hence
a in Sphere (
x,
r)
by TOPREAL9:9;
verum
end;
let a be object ; TARSKI:def 3 ( not a in Sphere (x,r) or a in (cl_Ball (x,r)) \ (Ball (x,r)) )
assume A5:
a in Sphere (x,r)
; a in (cl_Ball (x,r)) \ (Ball (x,r))
then reconsider a = a as Point of (TOP-REAL n) ;
A6:
|.(a - x).| = r
by A5, TOPREAL9:9;
then A7:
a in cl_Ball (x,r)
by TOPREAL9:8;
not a in Ball (x,r)
by A6, TOPREAL9:7;
hence
a in (cl_Ball (x,r)) \ (Ball (x,r))
by A7, XBOOLE_0:def 5; verum