let lambda, mu, nu be Real; ( 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 )
; ( 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 )
; verum