let n be Nat; :: thesis: for r being Real
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; :: 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 object ; :: 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:8;
dist (f,e) = r by A2, METRIC_1:13;
then |.(p - x).| = r by A1, JGRAPH_1:28;
hence q in Sphere (x,r) ; :: thesis: verum

end;

let q be object ; :: 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:8;
|.(q - x).| = r by A3, Th7;
then dist (f,e) = r by A1, JGRAPH_1:28;
hence q in Sphere (e,r) by METRIC_1:13; :: thesis: verum