let lambda, mu, nu be Real; :: thesis: ( lambda <> 1 & mu <> 1 & nu <> 1 implies ( 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) iff ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 ) )
set q = ((1 - lambda) * (1 - mu)) * (1 - nu);
assume ( lambda <> 1 & mu <> 1 & nu <> 1 ) ; :: thesis: ( 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) iff ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 )
then A1: ( 1 - lambda <> 0 & 1 - mu <> 0 & 1 - nu <> 0 ) ;
( 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) iff 0 = ((((1 - lambda) * (1 - mu)) * (1 - nu)) * 1) + (- ((mu * nu) * lambda)) ) ;
then ( 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) iff (((1 - lambda) * (1 - mu)) * (1 - nu)) * (1 + ((- ((lambda * mu) * nu)) / (((1 - lambda) * (1 - mu)) * (1 - nu)))) = 0 ) by A1, XCMPLX_1:235;
then ( 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) iff 1 + ((- ((lambda * mu) * nu)) / (((1 - lambda) * (1 - mu)) * (1 - nu))) = 0 ) by A1;
then ( 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) iff 1 + (- (((lambda * mu) * nu) / (((1 - lambda) * (1 - mu)) * (1 - nu)))) = 0 ) by XCMPLX_1:187;
then ( 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) iff 1 = (lambda * (mu * nu)) / ((1 - lambda) * ((1 - mu) * (1 - nu))) ) ;
then ( 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) iff 1 = ((lambda / (1 - lambda)) * (mu * nu)) / ((1 - mu) * (1 - nu)) ) by XCMPLX_1:83;
then ( 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) iff 1 = (lambda / (1 - lambda)) * ((mu * nu) / ((1 - mu) * (1 - nu))) ) by XCMPLX_1:74;
then ( 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) iff 1 = (lambda / (1 - lambda)) * (((mu / (1 - mu)) * nu) / (1 - nu)) ) by XCMPLX_1:83;
then ( 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) iff 1 = (lambda / (1 - lambda)) * ((mu / (1 - mu)) * (nu / (1 - nu))) ) by XCMPLX_1:74;
hence ( 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) iff ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 ) ; :: thesis: verum