set A = { (((1 - lambda) * p1) + (lambda * p2)) where lambda is Real : verum } ;
{ (((1 - lambda) * p1) + (lambda * p2)) where lambda is Real : verum } c= the carrier of (TOP-REAL n)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (((1 - lambda) * p1) + (lambda * p2)) where lambda is Real : verum } or x in the carrier of (TOP-REAL n) )
assume x in { (((1 - lambda) * p1) + (lambda * p2)) where lambda is Real : verum } ; :: thesis: x in the carrier of (TOP-REAL n)
then ex lambda being Real st x = ((1 - lambda) * p1) + (lambda * p2) ;
hence x in the carrier of (TOP-REAL n) ; :: thesis: verum

end;

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