theorem :: BKMODEL1:42

for P, Q being Element of (TOP-REAL 2)
for r being Real holds
( P in Sphere (Q,r) iff P in circle ((Q . 1),(Q . 2),r) )