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