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