theorem Th1: :: PROB_2:1

for r, r1, r2, r3 being Real st r <> 0 & r1 <> 0 holds
( r3 / r1 = r2 / r iff r3 * r = r2 * r1 )