theorem Th67a: :: GROUP_22:1

for a, b, c being Nat st c <> 0 & c * a divides c * b holds
a divides b by INT_4:7;