let V be RealLinearSpace; :: thesis: Up ((Omega). V) is convex
let u, v be VECTOR of V; :: according to CONVEX1:def 2 :: thesis: for r being Real st 0 < r & r < 1 & u in Up ((Omega). V) & v in Up ((Omega). V) holds
(r * u) + ((1 - r) * v) in Up ((Omega). V)
let r be Real; :: thesis: ( 0 < r & r < 1 & u in Up ((Omega). V) & v in Up ((Omega). V) implies (r * u) + ((1 - r) * v) in Up ((Omega). V) )
(Omega). V = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by RLSUB_1:def 4;
then (r * u) + ((1 - r) * v) in the carrier of ((Omega). V) ;
hence ( 0 < r & r < 1 & u in Up ((Omega). V) & v in Up ((Omega). V) implies (r * u) + ((1 - r) * v) in Up ((Omega). V) ) by RUSUB_4:def 5; :: thesis: verum