let n be Element of NAT ; :: thesis: for r being non negative real number
for p being Point of (TOP-REAL n) holds p is Point of (Tdisk p,r)
let r be non negative real number ; :: thesis: for p being Point of (TOP-REAL n) holds p is Point of (Tdisk p,r)
let p be Point of (TOP-REAL n); :: thesis: p is Point of (Tdisk p,r)
A1: the carrier of (Tdisk p,r) = cl_Ball p,r by BROUWER:3;
|.(p - p).| = 0 by TOPRNS_1:29;
hence p is Point of (Tdisk p,r) by A1, TOPREAL9:8; :: thesis: verum