{ (((1 - r) * v) + (r * w)) where r is Real : ( 0 <= r & r <= 1 ) } c= the carrier of X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (((1 - r) * v) + (r * w)) where r is Real : ( 0 <= r & r <= 1 ) } or x in the carrier of X )
assume x in { (((1 - r) * v) + (r * w)) where r is Real : ( 0 <= r & r <= 1 ) } ; :: thesis: x in the carrier of X
then ex r being Real st
( x = ((1 - r) * v) + (r * w) & 0 <= r & r <= 1 ) ;
hence x in the carrier of X ; :: thesis: verum

end;

hence { (((1 - r) * v) + (r * w)) where r is Real : ( 0 <= r & r <= 1 ) } is Subset of X ; :: thesis: verum