theorem Th1: :: KURATO_2:1

for n being Nat
for x being Point of (Euclid n)
for r being Real holds Ball (x,r) is open Subset of (TOP-REAL n) by TOPREAL3:8, GOBOARD6:3;