let n be 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 ex x9 being Element of REAL n st
( x = x9 & ex a19, a29, a39 being Real st
( (a19 + a29) + a39 = 1 & x9 = ((a19 * x1) + (a29 * x2)) + (a39 * x3) ) ) ;
hence ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) ; :: 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