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 that
A1: X is convex and
A2: B is convex ; :: thesis: ( X (O) B is convex & X (o) B is convex )
X (-) B is convex by A1, A2, Th76;
hence X (O) B is convex by A2, Th76; :: thesis: X (o) B is convex
X (+) B is convex by A1, A2, Th76;
hence X (o) B is convex by A2, Th76; :: thesis: verum