theorem Th51: :: DIOPHAN2:39

for a1, a2, b1, b2, c1, c2 being Element of REAL st |.((a1 * b2) - (a2 * b1)).| <> 0 & b2 <> 0 & a2 / b2 is rational holds
ex x, y being Element of INT st |.((LF (a1,b1,c1)) . (x,y)).| * |.((LF (a2,b2,c2)) . (x,y)).| <= |.((a1 * b2) - (a2 * b1)).| / 4