let n be Element of NAT ; :: thesis: for x being Point of (Euclid n)
for r being real number holds Ball (x,r) is open Subset of (TOP-REAL n)
let x be Point of (Euclid n); :: thesis: for r being real number holds Ball (x,r) is open Subset of (TOP-REAL n)
let r be real number ; :: thesis: Ball (x,r) is open Subset of (TOP-REAL n)
reconsider A = Ball (x,r) as Subset of (TOP-REAL n) by TOPREAL3:13;
reconsider A = A as Subset of (TOP-REAL n) ;
r is Real by XREAL_0:def 1;
then A is open by GOBOARD6:6;
hence Ball (x,r) is open Subset of (TOP-REAL n) ; :: thesis: verum