let a1, a2, b1, b2, c1, c2 be Element of REAL ; :: thesis: for eps being positive Real st |.((a1 * b2) - (a2 * b1)).| <> 0 & a2 / b2 is irrational holds
ex x, y being Element of INT st
( |.((LF (a2,b2,c2)) . (x,y)).| * |.((LF (a1,b1,c1)) . (x,y)).| < |.((a1 * b2) - (a2 * b1)).| / 4 & |.((LF (a2,b2,c2)) . (x,y)).| < eps )
let eps be positive Real; :: thesis: ( |.((a1 * b2) - (a2 * b1)).| <> 0 & a2 / b2 is irrational implies ex x, y being Element of INT st
( |.((LF (a2,b2,c2)) . (x,y)).| * |.((LF (a1,b1,c1)) . (x,y)).| < |.((a1 * b2) - (a2 * b1)).| / 4 & |.((LF (a2,b2,c2)) . (x,y)).| < eps ) )
|.((a2 * b1) - (a1 * b2)).| = |.(- ((a1 * b2) - (a2 * b1))).|
.= |.((a1 * b2) - (a2 * b1)).| by COMPLEX1:52 ;
hence ( |.((a1 * b2) - (a2 * b1)).| <> 0 & a2 / b2 is irrational implies ex x, y being Element of INT st
( |.((LF (a2,b2,c2)) . (x,y)).| * |.((LF (a1,b1,c1)) . (x,y)).| < |.((a1 * b2) - (a2 * b1)).| / 4 & |.((LF (a2,b2,c2)) . (x,y)).| < eps ) ) by Th46; :: thesis: verum