RelPrimes m c= Seg m by Th1;
hence RelPrimes m is finite ; :: thesis: verum