let p be Real; :: thesis: {p} is non empty closed_interval Subset of REAL
A1: {p} = [.p,p.] by XXREAL_1:17;
thus {p} is non empty closed_interval Subset of REAL by A1, MEASURE5:14; :: thesis: verum