RelPrimes m c= Seg m by Th1;
hence RelPrimes m is Subset of NAT by XBOOLE_1:1; :: thesis: verum