theorem Th46: :: DIOPHAN2:34

for a1, a2, b1, b2, c1, c2 being Element of REAL
for eps being positive Real st |.((a1 * b2) - (a2 * b1)).| <> 0 & a1 / b1 is irrational 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 & |.((LF (a1,b1,c1)) . (x,y)).| < eps )