let a, b be positive Real; :: thesis: ( a + b = 1 implies ((1 / (a ^2)) - 1) * ((1 / (b ^2)) - 1) >= 9 )
assume A1: a + b = 1 ; :: thesis: ((1 / (a ^2)) - 1) * ((1 / (b ^2)) - 1) >= 9
sqrt (a * b) > 0 by SQUARE_1:25;
then 1 ^2 >= (2 * (sqrt (a * b))) ^2 by A1, SIN_COS2:1, SQUARE_1:15;
then 1 >= (2 * 2) * ((sqrt (a * b)) ^2) ;
then 1 >= 4 * (a * b) by SQUARE_1:def 2;
then 8 / 1 <= 8 / ((4 * a) * b) by XREAL_1:118;
then 8 <= 8 / (4 * (a * b)) ;
then 8 <= (8 / 4) / (a * b) by XCMPLX_1:78;
then A2: 8 + 1 <= (2 / (a * b)) + 1 by XREAL_1:7;
((1 / (a ^2)) - 1) * ((1 / (b ^2)) - 1) = ((1 - (1 * (a ^2))) / (a ^2)) * ((1 / (b ^2)) - 1) by XCMPLX_1:126
.= ((1 - (1 * (a ^2))) / (a ^2)) * ((1 - (1 * (b ^2))) / (b ^2)) by XCMPLX_1:126
.= (((1 - a) * (1 + a)) * ((1 - b) * (1 + b))) / ((a ^2) * (b ^2)) by XCMPLX_1:76 ;
then ((1 / (a ^2)) - 1) * ((1 / (b ^2)) - 1) = ((a * b) * ((1 + a) * (1 + b))) / ((a * b) * (a * b)) by A1
.= ((a * b) / (a * b)) * (((1 + a) * (1 + b)) / (a * b)) by XCMPLX_1:76
.= 1 * (((1 + a) * (1 + b)) / (a * b)) by XCMPLX_1:60
.= ((1 + (a + b)) + (a * b)) / (a * b)
.= (2 / (a * b)) + ((a * b) / (a * b)) by A1, XCMPLX_1:62
.= (2 / (a * b)) + 1 by XCMPLX_1:60 ;
hence ((1 / (a ^2)) - 1) * ((1 / (b ^2)) - 1) >= 9 by A2; :: thesis: verum