reconsider a = x as Point of (Euclid 2) by TOPREAL3:13;
A1: x = |[(x `1 ),(x `2 )]| by EUCLID:57;
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:32; :: thesis: verum