let x be Element of REAL ; :: thesis: x is ext-real
x in REAL ;
hence x is ext-real by NUMBERS:31; :: thesis: verum