theorem Th43: :: DIOPHAN2:31

for a1, a2, b1, b2 being Element of REAL
for q, q1 being Element of RAT st |.((a1 * b2) - (a2 * b1)).| <> 0 & q <> q1 & (a2 * (denominator q)) + (b2 * (numerator q)) = 0 holds
(a2 * (denominator q1)) + (b2 * (numerator q1)) <> 0