for x being Element of R^1 holds x is real by TOPMETR:24;
hence R^1 is real-membered by Th18; :: thesis: verum