for p being Real holds {p} is non empty closed_interval Subset of REAL