let n be Element of NAT ; :: thesis: 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) ) )
let x, x1, x2, x3 be Element of REAL n; :: thesis: ( 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) ) )
thus ( x in plane x1,x2,x3 implies ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) ) :: thesis: ( ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) implies x in plane x1,x2,x3 )

proof

assume x in plane x1,x2,x3 ; :: thesis: ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) )
then consider x' being Element of REAL n such that
A1: ( x = x' & ex a1', a2', a3' being Real st
( (a1' + a2') + a3' = 1 & x' = ((a1' * x1) + (a2' * x2)) + (a3' * x3) ) ) ;
consider a1, a2, a3 being Real such that
A2: ( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) by A1;
thus ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) by A2; :: thesis: verum

end;

thus ( ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) implies x in plane x1,x2,x3 ) ; :: thesis: verum