theorem :: XREAL_1:71

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