theorem :: XREAL_1:170

for a, b, d being Real st 0 <= d & d <= 1 & 0 <= a & 0 <= b & (d * a) + ((1 - d) * b) = 0 & not ( d = 0 & b = 0 ) & not ( d = 1 & a = 0 ) holds
( a = 0 & b = 0 )