for m being Nat
for X being finite Subset of INT st 1 < m & card X = Euler m & ( for x, y being Integer st x in X & y in X & x <> y holds
not x,y are_congruent_mod m ) & ( for x being Integer st x in X holds
x,m are_coprime ) holds
X is_RRS_of m