let X be LinearTopSpace; :: thesis: for C being convex Subset of X holds Int C is convex
let C be convex Subset of X; :: thesis: Int C is convex

now :: thesis: for r being Real st 0 < r & r < 1 holds
(r * (Int C)) + ((1 - r) * (Int C)) c= Int C

let r be Real; :: thesis: ( 0 < r & r < 1 implies (r * (Int C)) + ((1 - r) * (Int C)) c= Int C )
assume that
A1: 0 < r and
A2: r < 1 ; :: thesis: (r * (Int C)) + ((1 - r) * (Int C)) c= Int C
(r * C) + ((1 - r) * C) c= C by A1, A2, CONVEX1:4;
then A3: Int ((r * C) + ((1 - r) * C)) c= Int C by TOPS_1:19;
0 + r < 1 by A2;
then 0 < 1 - r by XREAL_1:20;
then A4: (1 - r) * (Int C) = Int ((1 - r) * C) by Th51;
A5: (Int (r * C)) + (Int ((1 - r) * C)) c= Int ((r * C) + ((1 - r) * C)) by Th61;
Int (r * C) = r * (Int C) by A1, Th51;
hence (r * (Int C)) + ((1 - r) * (Int C)) c= Int C by A3, A5, A4; :: thesis: verum

end;

hence Int C is convex by CONVEX1:4; :: thesis: verum