let a, b, c, d be real positive number ; :: thesis: ((a * b) + (c * d)) * ((a * c) + (b * d)) >= (((4 * a) * b) * c) * d
((a * b) + (c * d)) * ((a * c) + (b * d)) = (((sqrt (a * b)) ^2 ) + (c * d)) * ((a * c) + (b * d)) by SQUARE_1:def 4
.= (((sqrt (a * b)) ^2 ) + ((sqrt (c * d)) ^2 )) * ((a * c) + (b * d)) by SQUARE_1:def 4
.= (((sqrt (a * b)) ^2 ) + ((sqrt (c * d)) ^2 )) * (((sqrt (a * c)) ^2 ) + (b * d)) by SQUARE_1:def 4
.= (((sqrt (a * b)) ^2 ) + ((sqrt (c * d)) ^2 )) * (((sqrt (a * c)) ^2 ) + ((sqrt (b * d)) ^2 )) by SQUARE_1:def 4 ;
then A1: ((a * b) + (c * d)) * ((a * c) + (b * d)) >= (b * c) * ((a + d) ^2 ) by Lm5;
sqrt (a * d) > 0 by SQUARE_1:93;
then 2 * (sqrt (a * d)) > 0 ;
then (a + d) ^2 >= (2 * (sqrt (a * d))) ^2 by SIN_COS2:1, SQUARE_1:77;
then (a + d) ^2 >= (2 ^2 ) * ((sqrt (a * d)) ^2 ) ;
then (a + d) ^2 >= (2 * 2) * (a * d) by SQUARE_1:def 4;
then ((a + d) ^2 ) * (b * c) >= ((4 * a) * d) * (b * c) by XREAL_1:66;
hence ((a * b) + (c * d)) * ((a * c) + (b * d)) >= (((4 * a) * b) * c) * d by A1, XXREAL_0:2; :: thesis: verum