reconsider a = x as Point of (Euclid 2) by TOPREAL3:8;
A1:
x = |[(x `1),(x `2)]|
by EUCLID:53;
Sphere (x,r) =
Sphere (a,r)
by TOPREAL9:15
.=
circle ((x `1),(x `2),r)
by A1, TOPREAL9:49
.=
{ w where w is Point of (TOP-REAL 2) : |.(w - |[(x `1),(x `2)]|).| = r }
by JGRAPH_6:def 5
;
hence
Sphere (x,r) is being_simple_closed_curve
by JGRAPH_6:23; verum