let n be Element of NAT ; :: thesis: for X, B being Subset of (TOP-REAL n) st X is convex & B is convex holds
( X (+) B is convex & X (-) B is convex )
let X, B be Subset of (TOP-REAL n); :: thesis: ( X is convex & B is convex implies ( X (+) B is convex & X (-) B is convex ) )
assume A1: ( X is convex & B is convex ) ; :: thesis: ( X (+) B is convex & X (-) B is convex )
thus X (+) B is convex :: thesis: X (-) B is convex

proof

for x, y being Point of (TOP-REAL n)
for r being real number st 0 <= r & r <= 1 & x in X (+) B & y in X (+) B holds
(r * x) + ((1 - r) * y) in X (+) B

proof

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

end;

hence X (+) B is convex by Def11; :: thesis: verum

end;

for x, y being Point of (TOP-REAL n)
for r being real number st 0 <= r & r <= 1 & x in X (-) B & y in X (-) B holds
(r * x) + ((1 - r) * y) in X (-) B

proof

let x, y be Point of (TOP-REAL n); :: thesis: for r being real number st 0 <= r & r <= 1 & x in X (-) B & y in X (-) B holds
(r * x) + ((1 - r) * y) in X (-) B
let r be real number ; :: thesis: ( 0 <= r & r <= 1 & x in X (-) B & y in X (-) B implies (r * x) + ((1 - r) * y) in X (-) B )
assume A6: ( 0 <= r & r <= 1 & x in X (-) B & y in X (-) B ) ; :: thesis: (r * x) + ((1 - r) * y) in X (-) B
then consider x1 being Point of (TOP-REAL n) such that
A7: ( x = x1 & B + x1 c= X ) ;
consider y1 being Point of (TOP-REAL n) such that
A8: ( y = y1 & B + y1 c= X ) by A6;
B + ((r * x) + ((1 - r) * y)) c= X

proof

let b1 be set ; :: according to TARSKI:def 3 :: thesis: ( not b1 in B + ((r * x) + ((1 - r) * y)) or b1 in X )
assume b1 in B + ((r * x) + ((1 - r) * y)) ; :: thesis: b1 in X
then consider b being Point of (TOP-REAL n) such that
A9: ( b1 = b + ((r * x) + ((1 - r) * y)) & b in B ) ;
A10: b + x in B + x by A9;
b + y in { (b2 + y) where b2 is Point of (TOP-REAL n) : b2 in B } by A9;
then (r * (b + x)) + ((1 - r) * (b + y)) in X by A1, A6, A7, A8, A10, Def11;
then ((r * b) + (r * x)) + ((1 - r) * (b + y)) in X by EUCLID:36;
then ((r * b) + (r * x)) + (((1 - r) * b) + ((1 - r) * y)) in X by EUCLID:36;
then (((r * b) + (r * x)) + ((1 - r) * b)) + ((1 - r) * y) in X by EUCLID:30;
then (((r * b) + (r * x)) + ((1 * b) - (r * b))) + ((1 - r) * y) in X by EUCLID:54;
then ((((r * b) + (r * x)) + (1 * b)) - (r * b)) + ((1 - r) * y) in X by EUCLID:49;
then ((((r * x) + (1 * b)) + (r * b)) - (r * b)) + ((1 - r) * y) in X by EUCLID:30;
then ((r * x) + (1 * b)) + ((1 - r) * y) in X by EUCLID:52;
then (1 * b) + ((r * x) + ((1 - r) * y)) in X by EUCLID:30;
hence b1 in X by A9, EUCLID:33; :: thesis: verum

end;

hence (r * x) + ((1 - r) * y) in X (-) B ; :: thesis: verum

end;

hence X (-) B is convex by Def11; :: thesis: verum