let d, a, b be real number ; :: thesis: ( 0 <= d & d <= 1 & 0 <= a & 0 <= b & (d * a) + ((1 - d) * b) = 0 & not ( d = 0 & b = 0 ) & not ( d = 1 & a = 0 ) implies ( a = 0 & b = 0 ) )
assume A1: ( 0 <= d & d <= 1 & a >= 0 & b >= 0 & (d * a) + ((1 - d) * b) = 0 ) ; :: thesis: ( ( d = 0 & b = 0 ) or ( d = 1 & a = 0 ) or ( a = 0 & b = 0 ) )
then d - d <= 1 - d by Lm7;
then ( ( d = 0 or a = 0 ) & ( 1 - d = 0 or b = 0 ) ) by A1;
hence ( ( d = 0 & b = 0 ) or ( d = 1 & a = 0 ) or ( a = 0 & b = 0 ) ) ; :: thesis: verum