theorem Th51: :: EUCLID_3:51

for n being Element of NAT
for p1, p2, p3, p0 being Point of (TOP-REAL n) st p2 - p1,p3 - p1 are_lindependent2 & p0 in plane (p1,p2,p3) holds
ex a1, a2, a3 being Real st
( p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) & (a1 + a2) + a3 = 1 & ( for b1, b2, b3 being Real st p0 = ((b1 * p1) + (b2 * p2)) + (b3 * p3) & (b1 + b2) + b3 = 1 holds
( b1 = a1 & b2 = a2 & b3 = a3 ) ) )