let x be Element of R; :: thesis: x is real
A1: the carrier of R c= REAL by Def1;
x in the carrier of R ;
then x is Element of REAL by A1;
hence x is real ; :: thesis: verum