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

proof

let x, y be Point of (TOP-REAL n); :: thesis: for r being real number st 0 <= r & r <= 1 & x in X ! & y in X ! holds
(r * x) + ((1 - r) * y) in X !
let r be real number ; :: thesis: ( 0 <= r & r <= 1 & x in X ! & y in X ! implies (r * x) + ((1 - r) * y) in X ! )
assume A2: ( 0 <= r & r <= 1 & x in X ! & y in X ! ) ; :: thesis: (r * x) + ((1 - r) * y) in X !
then consider x1 being Point of (TOP-REAL n) such that
A3: ( x = - x1 & x1 in X ) ;
consider x2 being Point of (TOP-REAL n) such that
A4: ( y = - x2 & x2 in X ) by A2;
(r * x1) + ((1 - r) * x2) in X by A1, A2, A3, A4, Def11;
then - ((r * x1) + ((1 - r) * x2)) in { (- z) where z is Point of (TOP-REAL n) : z in X } ;
then - ((r * x1) + ((1 - r) * x2)) in X ! ;
then (- (r * x1)) - ((1 - r) * x2) in X ! by EUCLID:42;
then (- (r * x1)) + (- ((1 - r) * x2)) in X ! by EUCLID:42;
then (r * (- x1)) + (- ((1 - r) * x2)) in X ! by EUCLID:44;
hence (r * x) + ((1 - r) * y) in X ! by A3, A4, EUCLID:44; :: thesis: verum

end;

hence X ! is convex by Def11; :: thesis: verum