let p be real number ; :: thesis: {p} is closed-interval Subset of REAL
A1: p is Real by XREAL_0:def 1;
{p} = [.p,p.] by XXREAL_1:17;
hence {p} is closed-interval Subset of REAL by A1, INTEGRA1:def 1; :: thesis: verum