let n be natural number ; :: thesis: for p being Point of (TOP-REAL n)
for r being real number holds the carrier of (Tball (p,r)) = Ball (p,r)
let p be Point of (TOP-REAL n); :: thesis: for r being real number holds the carrier of (Tball (p,r)) = Ball (p,r)
let r be real number ; :: thesis: the carrier of (Tball (p,r)) = Ball (p,r)
[#] (Tball (p,r)) = Ball (p,r) by PRE_TOPC:def 10;
hence the carrier of (Tball (p,r)) = Ball (p,r) ; :: thesis: verum