let m be Nat; :: thesis: ( 1 <= m implies RelPrimes m <> {} )
assume A1: 1 <= m ; :: thesis: RelPrimes m <> {}
m gcd 1 = 1 by NEWTON:51;
then m,1 are_coprime by INT_2:def 3;
then 1 in RelPrimes m by A1;
hence RelPrimes m <> {} ; :: thesis: verum