theorem Th49: :: DIOPHAN2:37

for a1, a2, b1, b2, c1, c2 being Element of REAL st ZeroPointSet (LF (a2,b2,c2)) <> {} holds
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