let n be Element of NAT ; :: thesis: for r being real number
for x being Point of (TOP-REAL n) holds the carrier of (Tdisk x,r) = cl_Ball x,r
let r be real number ; :: thesis: for x being Point of (TOP-REAL n) holds the carrier of (Tdisk x,r) = cl_Ball x,r
let x be Point of (TOP-REAL n); :: thesis: the carrier of (Tdisk x,r) = cl_Ball x,r
[#] (Tdisk x,r) = cl_Ball x,r by PRE_TOPC:def 10;
hence the carrier of (Tdisk x,r) = cl_Ball x,r ; :: thesis: verum