theorem Th13: :: BROUWER3:13

for n being Nat
for p being Point of (TOP-REAL n)
for r being Real st r > 0 holds
for U being Subset of (Tdisk (p,r)) st U is open & not U is empty holds
for A being Subset of (TOP-REAL n) st A = U holds
not Int A is empty