for p being Element of (TOP-REAL 1) ex r being Real st p = <*r*>