let a1, a2, b1, b2, c1, c2 be Element of REAL ; :: thesis: ( ZeroPointSet (LF (a2,b2,c2)) <> {} 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 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
then consider p being object such that
A2: p in ZeroPointSet (LF (a2,b2,c2)) by XBOOLE_0:def 1;
( (LF (a2,b2,c2)) . p = 0 & p in dom (LF (a2,b2,c2)) ) by A2, Th13;
then consider p1, p2 being object such that
A4: ( p1 in INT & p2 in INT & p = [p1,p2] ) by ZFMISC_1:def 2;
reconsider x = p1, y = p2 as Element of INT by A4;
(LF (a2,b2,c2)) . (x,y) = 0 by A2, Th13, A4;
then |.((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 ; :: thesis: verum