theorem Th5: :: GOBOARD6:5

for n being Nat
for u being Point of (Euclid n)
for P being Subset of (TOP-REAL n) holds
( u in Int P iff ex r being Real st
( r > 0 & Ball (u,r) c= P ) )