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 (O) B is convex & X (o) B is convex )
let X, B be Subset of (TOP-REAL n); :: thesis: ( X is convex & B is convex implies ( X (O) B is convex & X (o) B is convex ) )
assume A1: ( X is convex & B is convex ) ; :: thesis: ( X (O) B is convex & X (o) B is convex )
thus X (O) B is convex :: thesis: X (o) B is convex

proof

X (-) B is convex by A1, Th77;
hence X (O) B is convex by A1, Th77; :: thesis: verum

end;

X (+) B is convex by A1, Th77;
hence X (o) B is convex by A1, Th77; :: thesis: verum