let a1, a2, b1, b2, c1, c2 be Element of REAL ; :: thesis: ( ZeroPointSet (LF (a1,b1,c1)) <> {} 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 (a1,b1,c1)) <> {} ; :: 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 (a1,b1,c1)) by XBOOLE_0:def 1;

( (LF (a1,b1,c1)) . p = 0 & p in dom (LF (a1,b1,c1)) ) 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 (a1,b1,c1)) . (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

assume ZeroPointSet (LF (a1,b1,c1)) <> {} ; :: 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 (a1,b1,c1)) by XBOOLE_0:def 1;

( (LF (a1,b1,c1)) . p = 0 & p in dom (LF (a1,b1,c1)) ) 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 (a1,b1,c1)) . (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