set A = { x where x is Element of REAL n : ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) } ;
{ x where x is Element of REAL n : ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) } c= REAL n

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is Element of REAL n : ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) } or x in REAL n )
assume x in { x where x is Element of REAL n : ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) } ; :: thesis: x in REAL n
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) ) ) ;
thus x in REAL n by A1; :: thesis: verum

end;

hence { x where x is Element of REAL n : ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) } is Subset of (REAL n) ; :: thesis: verum