let n be Element of NAT ; :: thesis: for r being non negative Real
for p being Point of (TOP-REAL n) holds p is Point of (Tdisk (p,r))
let r be non negative Real; :: 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:28;
hence p is Point of (Tdisk (p,r)) by A1, TOPREAL9:8; :: thesis: verum