theorem Th50: :: DIOPHAN2:38

for a1, a2, b1, b2, c1, c2 being Element of REAL st |.((a1 * b2) - (a2 * b1)).| <> 0 & b1 <> 0 & a1 / b1 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