let n be Element of NAT ; :: thesis:
let X be Subset of (TOP-REAL n); :: thesis:
assume A1: X is convex ; :: thesis:
for x, y being Point of (TOP-REAL n)
for r being Real st 0 <= r & r <= 1 & x in X ! & y in X ! holds
(r * x) + ((1 - r) * y) in X !

let x, y be Point of (TOP-REAL n); :: thesis:
let r be Real; :: thesis:
assume that
A2: ( 0 <= r & r <= 1 ) and
A3: x in X ! and
A4: y in X ! ; :: thesis:
consider x2 being Point of (TOP-REAL n) such that
A5: y = - x2 and
A6: x2 in X by A4;
consider x1 being Point of (TOP-REAL n) such that
A7: x = - x1 and
A8: x1 in X by A3;
(r * x1) + ((1 - r) * x2) in X by A1, A2, A8, A6;
then - ((r * x1) + ((1 - r) * x2)) in X ! ;
then (- (r * x1)) - ((1 - r) * x2) in X ! by RLVECT_1:30;
then (r * (- x1)) + (- ((1 - r) * x2)) in X ! by RLVECT_1:25;
hence (r * x) + ((1 - r) * y) in X ! by A7, A5, RLVECT_1:25; :: thesis:

end;