let a, b, c, d be real positive number ; (((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:9;
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:89;
(((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 4
.=
((a * b) + (c * d)) * (((sqrt (a * c)) ^2 ) + ((sqrt (b * d)) ^2 ))
by SQUARE_1:def 4
.=
((a * b) + (c * d)) * ((a * c) + ((sqrt (b * d)) ^2 ))
by SQUARE_1:def 4
.=
((a * b) + (c * d)) * ((a * c) + (b * d))
by SQUARE_1:def 4
.=
(((((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