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