let n be Element of NAT ; :: thesis: for r being real number
for x being Point of (TOP-REAL n)
for e being Point of (Euclid n) st x = e holds
Sphere e,r = Sphere x,r
let r be real number ; :: thesis: for x being Point of (TOP-REAL n)
for e being Point of (Euclid n) st x = e holds
Sphere e,r = Sphere x,r
let x be Point of (TOP-REAL n); :: thesis: for e being Point of (Euclid n) st x = e holds
Sphere e,r = Sphere x,r
let e be Point of (Euclid n); :: thesis: ( x = e implies Sphere e,r = Sphere x,r )
assume A1: x = e ; :: thesis: Sphere e,r = Sphere x,r

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: Sphere x,r c= Sphere e,r

let q be set ; :: thesis: ( q in Sphere e,r implies q in Sphere x,r )
assume A2: q in Sphere e,r ; :: thesis: q in Sphere x,r
then reconsider f = q as Point of (Euclid n) ;
reconsider p = f as Point of (TOP-REAL n) by TOPREAL3:13;
dist f,e = r by A2, METRIC_1:14;
then |.(p - x).| = r by A1, JGRAPH_1:45;
hence q in Sphere x,r ; :: thesis: verum

end;

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in Sphere x,r or q in Sphere e,r )
assume A3: q in Sphere x,r ; :: thesis: q in Sphere e,r
then reconsider q = q as Point of (TOP-REAL n) ;
reconsider f = q as Point of (Euclid n) by TOPREAL3:13;
|.(q - x).| = r by A3, Th9;
then dist f,e = r by A1, JGRAPH_1:45;
hence q in Sphere e,r by METRIC_1:14; :: thesis: verum