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 V

proof

let x be object ; :: 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 V )
assume x in { (((1 - l) * p) + (l * q)) where l is Real : 0 <= l } ; :: thesis: x in the carrier of V
then ex l being Real st
( x = ((1 - l) * p) + (l * q) & 0 <= l ) ;
hence x in the carrier of V ; :: thesis: verum

end;

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