let a, b, c be positive Real; :: thesis: ( (a + b) + c = 1 implies 1 + (1 / a) = 2 + ((b + c) / a) )
assume (a + b) + c = 1 ; :: thesis: 1 + (1 / a) = 2 + ((b + c) / a)
then 1 + (1 / a) = 1 + ((a + (b + c)) / a)
.= 1 + ((a / a) + ((b + c) / a)) by XCMPLX_1:62
.= (1 + (a / a)) + ((b + c) / a)
.= (1 + 1) + ((b + c) / a) by XCMPLX_1:60 ;
hence 1 + (1 / a) = 2 + ((b + c) / a) ; :: thesis: verum