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