let a1, a2, b1, b2, c1, c2 be Element of REAL ; :: thesis: ( |.((a1 * b2) - (a2 * b1)).| <> 0 & b2 <> 0 & a2 / b2 is rational implies 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 )
assume A1: ( |.((a1 * b2) - (a2 * b1)).| <> 0 & b2 <> 0 & a2 / b2 is rational ) ; :: thesis: 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
A4: |.((a2 * b1) - (a1 * b2)).| = |.(- ((a1 * b2) - (a2 * b1))).|
.= |.((a1 * b2) - (a2 * b1)).| by COMPLEX1:52 ;
then ex x, y being Element of INT st |.((LF (a2,b2,c2)) . (x,y)).| * |.((LF (a1,b1,c1)) . (x,y)).| <= |.((a2 * b1) - (a1 * b2)).| / 4 by A1, Th50;
hence 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 by A4; :: thesis: verum