theorem :: EUCLIDLP:87

for a1, a2, a3 being Real
for n being Nat
for x, x1, x2, x3 being Element of REAL n st x in plane (x1,x2,x3) & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & not (a1 + a2) + a3 = 1 holds
0* n in plane (x1,x2,x3)