let a1, a2, b1, b2, c1, c2 be Element of REAL ; :: thesis: ( |.((a1 * b2) - (a2 * b1)).| <> 0 & b1 = 0 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 )
set Delta = |.((a1 * b2) - (a2 * b1)).|;
assume that
A1: |.((a1 * b2) - (a2 * b1)).| <> 0 and
A2: b1 = 0 ; :: 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: b2 <> 0 by A1, A2;

per cases ( ( a2 / b2 is irrational & ZeroPointSet (LF (a2,b2,c2)) = {} ) or ZeroPointSet (LF (a2,b2,c2)) <> {} or ( a2 / b2 is rational & ZeroPointSet (LF (a2,b2,c2)) = {} ) ) ;

suppose A5: ( a2 / b2 is irrational & ZeroPointSet (LF (a2,b2,c2)) = {} ) ; :: 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

for eps being positive Real 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

proof

let eps be positive Real; :: 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
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 A1, A5, Th47;
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 ; :: thesis: verum

end;

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 ; :: thesis: verum

end;

suppose ZeroPointSet (LF (a2,b2,c2)) <> {} ; :: 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

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 Th49; :: thesis: verum

end;

suppose ( a2 / b2 is rational & ZeroPointSet (LF (a2,b2,c2)) = {} ) ; :: 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

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 A1, A4, Th51; :: thesis: verum

end;

end;