( not ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1)) is boundary & ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1)) is convex & ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1)) is compact ) ;
hence ex b₁ being Subset of (TOP-REAL n) st
( not b₁ is boundary & b₁ is convex & b₁ is compact ) ; :: thesis: verum