let V be RealLinearSpace; :: thesis: Up ((0). 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 ((0). V) & v in Up ((0). V) holds
(r * u) + ((1 - r) * v) in Up ((0). V)
let r be Real; :: thesis: ( 0 < r & r < 1 & u in Up ((0). V) & v in Up ((0). V) implies (r * u) + ((1 - r) * v) in Up ((0). V) )
assume that
0 < r and
r < 1 and
A1: u in Up ((0). V) and
A2: v in Up ((0). V) ; :: thesis: (r * u) + ((1 - r) * v) in Up ((0). V)
v in the carrier of ((0). V) by A2, RUSUB_4:def 5;
then v in {(0. V)} by RLSUB_1:def 3;
then A3: v = 0. V by TARSKI:def 1;
u in the carrier of ((0). V) by A1, RUSUB_4:def 5;
then u in {(0. V)} by RLSUB_1:def 3;
then u = 0. V by TARSKI:def 1;
then (r * u) + ((1 - r) * v) = (0. V) + ((1 - r) * (0. V)) by A3
.= (0. V) + (0. V)
.= 0. V ;
then (r * u) + ((1 - r) * v) in {(0. V)} by TARSKI:def 1;
then (r * u) + ((1 - r) * v) in the carrier of ((0). V) by RLSUB_1:def 3;
hence (r * u) + ((1 - r) * v) in Up ((0). V) by RUSUB_4:def 5; :: thesis: verum