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