theorem Th41: :: TOPREAL6:43

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
proj1 .: P = ].((p `1) - r),((p `1) + r).[