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 A1: ( 0 <= r & r <= 1 & 0. X in M ) ; :: thesis: r * M c= M
let x be object ; :: 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
A2: r * v = x and
A3: v in M ;
(r * v) + ((1 - r) * (0. X)) in M by A1, A3, Def1;
then (r * v) + (0. X) in M ;
hence x in M by A2; :: thesis: verum