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