the carrier of MS c= REALPLUS by Def07a;
hence r is positive Real by Th1; :: thesis: verum