for a, b, c, d being positive Real holds ((a * b) + (c * d)) * ((a * c) + (b * d)) >= (((4 * a) * b) * c) * d