let X be RealLinearSpace; :: thesis: for M being convex Subset of X
for r being Real st 0 <= r & r <= 1 & 0. X in M holds
r * M c= M
let M be convex Subset of X; :: thesis: for r being Real st 0 <= r & r <= 1 & 0. X in M holds
r * M c= M
let r be Real; :: thesis: ( 0 <= r & r <= 1 & 0. X in M implies r * M c= M )
assume that
A1: 0 <= r and
A2: r <= 1 and
A3: 0. X in M ; :: thesis: r * M c= M
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in r * M or x in M )
assume x in r * M ; :: thesis: x in M
then consider v being Point of X such that
A4: r * v = x and
A5: v in M ;
(r * v) + ((1 - r) * (0. X)) in M by A1, A2, A3, A5, Def1;
then (r * v) + (0. X) in M by RLVECT_1:23;
hence x in M by A4, RLVECT_1:def 7; :: thesis: verum