A1: ex e being Point of (Euclid n) st
( p = e & OpenHypercube (p,r) = OpenHypercube (e,r) ) by Def1;
OpenHypercube (p,r) c= Int (ClosedHypercube (p,(n |-> r))) by Th12, TOPS_1:24;
hence not ClosedHypercube (p,(n |-> r)) is boundary by A1; :: thesis: verum