for x being Element of REAL 1 ex rx being Real st x = <*rx*>