let a, b, r be Real; for x being Point of (Euclid 2) st x = |[a,b]| holds
Sphere (x,r) = circle (a,b,r)
let x be Point of (Euclid 2); ( x = |[a,b]| implies Sphere (x,r) = circle (a,b,r) )
assume A1:
x = |[a,b]|
; Sphere (x,r) = circle (a,b,r)
hereby TARSKI:def 3,
XBOOLE_0:def 10 circle (a,b,r) c= Sphere (x,r)
let w be
object ;
( w in Sphere (x,r) implies w in circle (a,b,r) )assume A2:
w in Sphere (
x,
r)
;
w in circle (a,b,r)then reconsider u =
w as
Point of
(TOP-REAL 2) by TOPREAL3:8;
reconsider e =
u as
Point of
(Euclid 2) by TOPREAL3:8;
dist (
e,
x)
= |.(u - |[a,b]|).|
by A1, JGRAPH_1:28;
then
|.(u - |[a,b]|).| = r
by A2, METRIC_1:13;
hence
w in circle (
a,
b,
r)
by Th41;
verum
end;
let w be object ; TARSKI:def 3 ( not w in circle (a,b,r) or w in Sphere (x,r) )
assume A3:
w in circle (a,b,r)
; w in Sphere (x,r)
then reconsider u = w as Point of (TOP-REAL 2) ;
reconsider e = u as Point of (Euclid 2) by TOPREAL3:8;
dist (e,x) = |.(u - |[a,b]|).|
by A1, JGRAPH_1:28;
then
dist (e,x) = r
by A3, Th41;
hence
w in Sphere (x,r)
by METRIC_1:13; verum