let x be Element of REAL 1; :: thesis: ex rx being Real st x = <*rx*>
x is Element of (TOP-REAL 1) by EUCLID:22;
then consider rx being Real such that
A1: x = <*rx*> by JORDAN2B:20;
thus ex rx being Real st x = <*rx*> by A1; :: thesis: verum