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; :: thesis: verum

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; :: thesis: verum