theorem Th20: :: JORDAN2B:20

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