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 that
A1: X is convex and
A2: B is convex ; :: thesis: ( X (+) B is convex & X (-) B is convex )
for x, y being Point of (TOP-REAL n)
for r being Real 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 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; :: thesis: ( 0 <= r & r <= 1 & x in X (+) B & y in X (+) B implies (r * x) + ((1 - r) * y) in X (+) B )
assume that
A3: ( 0 <= r & r <= 1 ) and
A4: x in X (+) B and
A5: y in X (+) B ; :: thesis: (r * x) + ((1 - r) * y) in X (+) B
consider x2, b2 being Point of (TOP-REAL n) such that
A6: y = x2 + b2 and
A7: ( x2 in X & b2 in B ) by A5;
consider x1, b1 being Point of (TOP-REAL n) such that
A8: x = x1 + b1 and
A9: ( x1 in X & b1 in B ) by A4;
( (r * x1) + ((1 - r) * x2) in X & (r * b1) + ((1 - r) * b2) in B ) by A1, A2, A3, A9, A7;
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 ) } ;
then (((r * x1) + ((1 - r) * x2)) + (r * b1)) + ((1 - r) * b2) in X (+) B by RLVECT_1:def 3;
then (((r * x1) + (r * b1)) + ((1 - r) * x2)) + ((1 - r) * b2) in X (+) B by RLVECT_1:def 3;
then ((r * x1) + (r * b1)) + (((1 - r) * x2) + ((1 - r) * b2)) in X (+) B by RLVECT_1:def 3;
then (r * (x1 + b1)) + (((1 - r) * x2) + ((1 - r) * b2)) in X (+) B by RLVECT_1:def 5;
hence (r * x) + ((1 - r) * y) in X (+) B by A8, A6, RLVECT_1:def 5; :: thesis: verum

end;

hence X (+) B is convex ; :: thesis: X (-) B is convex
for x, y being Point of (TOP-REAL n)
for r being Real 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 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; :: thesis: ( 0 <= r & r <= 1 & x in X (-) B & y in X (-) B implies (r * x) + ((1 - r) * y) in X (-) B )
assume that
A10: ( 0 <= r & r <= 1 ) and
A11: ( x in X (-) B & y in X (-) B ) ; :: thesis: (r * x) + ((1 - r) * y) in X (-) B
A12: ( ex x1 being Point of (TOP-REAL n) st
( x = x1 & B + x1 c= X ) & ex y1 being Point of (TOP-REAL n) st
( y = y1 & B + y1 c= X ) ) by A11;
B + ((r * x) + ((1 - r) * y)) c= X

proof

let b1 be object ; :: 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
A13: b1 = b + ((r * x) + ((1 - r) * y)) and
A14: b in B ;
( b + x in B + x & b + y in { (b2 + y) where b2 is Point of (TOP-REAL n) : b2 in B } ) by A14;
then (r * (b + x)) + ((1 - r) * (b + y)) in X by A1, A10, A12;
then ((r * b) + (r * x)) + ((1 - r) * (b + y)) in X by RLVECT_1:def 5;
then ((r * b) + (r * x)) + (((1 - r) * b) + ((1 - r) * y)) in X by RLVECT_1:def 5;
then (((r * b) + (r * x)) + ((1 - r) * b)) + ((1 - r) * y) in X by RLVECT_1:def 3;
then (((r * b) + (r * x)) + ((1 * b) - (r * b))) + ((1 - r) * y) in X by RLVECT_1:35;
then ((((r * b) + (r * x)) + (1 * b)) - (r * b)) + ((1 - r) * y) in X by RLVECT_1:def 3;
then ((((r * x) + (1 * b)) + (r * b)) - (r * b)) + ((1 - r) * y) in X by RLVECT_1:def 3;
then ((r * x) + (1 * b)) + ((1 - r) * y) in X by RLVECT_4:1;
then (1 * b) + ((r * x) + ((1 - r) * y)) in X by RLVECT_1:def 3;
hence b1 in X by A13, RLVECT_1:def 8; :: thesis: verum

end;

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

end;

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