theorem Th33: :: BKMODEL4:5

for a, b, c, d being Real st b <> 0 holds
(((a * b) / c) * d) / b = (a * d) / c