let a, b, c, d be positive Real; ((a * b) + (c * d)) * ((a * c) + (b * d)) >= (((4 * a) * b) * c) * d
sqrt (a * d) > 0
by SQUARE_1:25;
then
(a + d) ^2 >= (2 * (sqrt (a * d))) ^2
by SIN_COS2:1, SQUARE_1:15;
then
(a + d) ^2 >= (2 ^2) * ((sqrt (a * d)) ^2)
;
then
(a + d) ^2 >= (2 * 2) * (a * d)
by SQUARE_1:def 2;
then A1:
((a + d) ^2) * (b * c) >= ((4 * a) * d) * (b * c)
by XREAL_1:64;
((a * b) + (c * d)) * ((a * c) + (b * d)) =
(((sqrt (a * b)) ^2) + (c * d)) * ((a * c) + (b * d))
by SQUARE_1:def 2
.=
(((sqrt (a * b)) ^2) + ((sqrt (c * d)) ^2)) * ((a * c) + (b * d))
by SQUARE_1:def 2
.=
(((sqrt (a * b)) ^2) + ((sqrt (c * d)) ^2)) * (((sqrt (a * c)) ^2) + (b * d))
by SQUARE_1:def 2
.=
(((sqrt (a * b)) ^2) + ((sqrt (c * d)) ^2)) * (((sqrt (a * c)) ^2) + ((sqrt (b * d)) ^2))
by SQUARE_1:def 2
;
then
((a * b) + (c * d)) * ((a * c) + (b * d)) >= (b * c) * ((a + d) ^2)
by Lm5;
hence
((a * b) + (c * d)) * ((a * c) + (b * d)) >= (((4 * a) * b) * c) * d
by A1, XXREAL_0:2; verum