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

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

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

end;

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