let n be Element of NAT ; :: thesis: for p being Point of (TOP-REAL n) holds {p} is bounded
let p be Point of (TOP-REAL n); :: thesis: {p} is bounded
reconsider a = p as Point of (Euclid n) by EUCLID:67;
{a} is bounded by TBSP_1:15;
hence {p} is bounded by JORDAN2C:11; :: thesis: verum