for a, b, m, x being Integer st m <> 0 & ((a * x) - b) mod m = 0 holds
for y being Integer holds
( ( a,m are_coprime & ((a * y) - b) mod m = 0 implies y in Class ((Cong m),x) ) & ( y in Class ((Cong m),x) implies ((a * y) - b) mod m = 0 ) )