let a, b, r be real number ; :: thesis: 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); :: thesis: ( x = |[a,b]| implies Sphere x,r = circle a,b,r )
assume A1: x = |[a,b]| ; :: thesis: Sphere x,r = circle a,b,r

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

let w be set ; :: thesis: ( w in Sphere x,r implies w in circle a,b,r )
assume A2: w in Sphere x,r ; :: thesis: w in circle a,b,r
then reconsider u = w as Point of (TOP-REAL 2) by TOPREAL3:13;
reconsider e = u as Point of (Euclid 2) by TOPREAL3:13;
dist e,x = |.(u - |[a,b]|).| by A1, JGRAPH_1:45;
then |.(u - |[a,b]|).| = r by A2, METRIC_1:14;
hence w in circle a,b,r by Th43; :: thesis: verum

end;

let w be set ; :: according to TARSKI:def 3 :: thesis: ( not w in circle a,b,r or w in Sphere x,r )
assume A3: w in circle a,b,r ; :: thesis: 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:13;
dist e,x = |.(u - |[a,b]|).| by A1, JGRAPH_1:45;
then dist e,x = r by A3, Th43;
hence w in Sphere x,r by METRIC_1:14; :: thesis: verum