theorem :: BORSUK_4:20

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