set A = { (((1 - r) * v) + (r * w)) where r is Real : verum } ;
{ (((1 - r) * v) + (r * w)) where r is Real : verum } c= the carrier of V
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (((1 - r) * v) + (r * w)) where r is Real : verum } or x in the carrier of V )
assume x in { (((1 - r) * v) + (r * w)) where r is Real : verum } ; :: thesis: x in the carrier of V
then ex r being Real st x = ((1 - r) * v) + (r * w) ;
hence x in the carrier of V ; :: thesis: verum
end;
hence { (((1 - r) * v) + (r * w)) where r is Real : verum } is Subset of V ; :: thesis: verum