let n be Element of NAT ; :: thesis: for r being Real

for x being Point of (TOP-REAL n) holds the carrier of (Tdisk (x,r)) = cl_Ball (x,r)

let r be Real; :: 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 5;

hence the carrier of (Tdisk (x,r)) = cl_Ball (x,r) ; :: thesis: verum

for x being Point of (TOP-REAL n) holds the carrier of (Tdisk (x,r)) = cl_Ball (x,r)

let r be Real; :: 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 5;

hence the carrier of (Tdisk (x,r)) = cl_Ball (x,r) ; :: thesis: verum