set X = { (((1 - l) * p) + (l * q)) where l is Real : 0 <= l } ;
{ (((1 - l) * p) + (l * q)) where l is Real : 0 <= l } c= the carrier of (TOP-REAL n)

proof

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

end;

hence { (((1 - l) * p) + (l * q)) where l is Real : 0 <= l } is Subset of (TOP-REAL n) ; :: thesis: verum