set A = { (((1 - lambda) * x1) + (lambda * x2)) where lambda is Real : verum } ;
{ (((1 - lambda) * x1) + (lambda * x2)) where lambda is Real : verum } c= REAL n

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (((1 - lambda) * x1) + (lambda * x2)) where lambda is Real : verum } or x in REAL n )
assume x in { (((1 - lambda) * x1) + (lambda * x2)) where lambda is Real : verum } ; :: thesis: x in REAL n
then ex lambda being Real st x = ((1 - lambda) * x1) + (lambda * x2) ;
hence x in REAL n ; :: thesis: verum

end;

hence { (((1 - lambda) * x1) + (lambda * x2)) where lambda is Real : verum } is Subset of (REAL n) ; :: thesis: verum