theorem Th28: :: NUMBER17:28

for x, y, n being Nat st n > 0 & x >= y holds
( x,y are_congruent_mod n iff ex k being Nat st x = (k * n) + y )