RelPrimes m c= Seg m by Th1;
hence RelPrimes m is included_in_Seg by FINSEQ_1:def 13; :: thesis: verum