theorem Th28: :: EUCLIDLP:28

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