theorem Th13: :: INT_4:13

for b being Integer st b > 0 holds
for a being Integer ex q, r being Integer st
( a = (b * q) + r & r >= 0 & r < b )