for p being Point of (TOP-REAL 2)
for e being Point of (Euclid 2)
for P being Subset of (TOP-REAL 2)
for r being Real st P = Ball (e,r) & p = e holds
proj2 .: P = ].((p `2) - r),((p `2) + r).[