( {} in RAT+ & one in RAT+ ) ;
hence ( {} in REAL+ & one in REAL+ ) by Th1; :: thesis: verum