let x be Element of INT.Ring ; :: thesis: x in REAL
x in INT ;
hence x in REAL by NUMBERS:15; :: thesis: verum