let a, b be positive Real; :: thesis: ( a + b = 1 implies (1 + (1 / a)) * (1 + (1 / b)) >= 9 )
assume A1: a + b = 1 ; :: thesis: (1 + (1 / a)) * (1 + (1 / b)) >= 9
then 1 / (a * b) >= 1 / (1 / 4) by Th18, XREAL_1:85;
then (1 / (a * b)) * (- 2) <= 4 * (- 2) by XREAL_1:65;
then - ((1 / (a * b)) * 2) <= - 8 ;
then (1 / (a * b)) * 2 >= 8 by XREAL_1:24;
then A2: 1 + (2 * (1 / (a * b))) >= 1 + 8 by XREAL_1:7;
(1 + (1 / a)) * (1 + (1 / b)) = (((1 * 1) + (1 * (1 / b))) + ((1 / a) * (1 / b))) + ((1 / a) * 1)
.= ((1 + (1 / b)) + (1 / (a * b))) + (1 / a) by XCMPLX_1:102
.= (1 + ((1 / b) + (1 / a))) + (1 / (a * b))
.= (1 + (((1 * a) + (b * 1)) / (a * b))) + (1 / (a * b)) by XCMPLX_1:116
.= (1 + (1 / (a * b))) + (1 / (a * b)) by A1
.= 1 + (2 * (1 / (a * b))) ;
hence (1 + (1 / a)) * (1 + (1 / b)) >= 9 by A2; :: thesis: verum