for r being Real
for s being Point of (TOP-REAL 2) st s in Sphere ((0. (TOP-REAL 2)),r) holds
((s `1) ^2) + ((s `2) ^2) = r ^2