let a, b, c, d be positive Real; (((sqrt (a * b)) ^2) + ((sqrt (c * d)) ^2)) * (((sqrt (a * c)) ^2) + ((sqrt (b * d)) ^2)) >= (b * c) * ((a + d) ^2)
((a * (b ^2)) * d) + (((c ^2) * d) * a) >= 2 * (sqrt (((a * (b ^2)) * d) * (((c ^2) * d) * a)))
by SIN_COS2:1;
then
(((a * (b ^2)) * d) + (((c ^2) * d) * a)) + ((((a ^2) * b) * c) + ((b * c) * (d ^2))) >= (2 * (sqrt ((((a ^2) * (b ^2)) * (c ^2)) * (d ^2)))) + ((((a ^2) * b) * c) + ((b * c) * (d ^2)))
by XREAL_1:7;
then
((((a * (b ^2)) * d) + (((c ^2) * d) * a)) + (((a ^2) * b) * c)) + ((b * c) * (d ^2)) >= ((2 * (sqrt (((a * b) * (c * d)) ^2))) + (((a ^2) * b) * c)) + ((b * c) * (d ^2))
;
then A1:
((((a * (b ^2)) * d) + (((c ^2) * d) * a)) + (((a ^2) * b) * c)) + ((b * c) * (d ^2)) >= ((2 * (((a * b) * c) * d)) + (((a ^2) * b) * c)) + ((b * c) * (d ^2))
by SQUARE_1:22;
(((sqrt (a * b)) ^2) + ((sqrt (c * d)) ^2)) * (((sqrt (a * c)) ^2) + ((sqrt (b * d)) ^2)) =
((a * b) + ((sqrt (c * d)) ^2)) * (((sqrt (a * c)) ^2) + ((sqrt (b * d)) ^2))
by SQUARE_1:def 2
.=
((a * b) + (c * d)) * (((sqrt (a * c)) ^2) + ((sqrt (b * d)) ^2))
by SQUARE_1:def 2
.=
((a * b) + (c * d)) * ((a * c) + ((sqrt (b * d)) ^2))
by SQUARE_1:def 2
.=
((a * b) + (c * d)) * ((a * c) + (b * d))
by SQUARE_1:def 2
.=
(((((a ^2) * b) * c) + ((a * (b ^2)) * d)) + (((c ^2) * d) * a)) + ((b * c) * (d ^2))
;
hence
(((sqrt (a * b)) ^2) + ((sqrt (c * d)) ^2)) * (((sqrt (a * c)) ^2) + ((sqrt (b * d)) ^2)) >= (b * c) * ((a + d) ^2)
by A1; verum