reconsider e = p as Point of (Euclid n) by EUCLID:67;
A1: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider O = OpenHypercube (e,r) as Subset of (TOP-REAL n) ;
OpenHypercube (e,r) in the topology of (TOP-REAL n) by PRE_TOPC:def 2, A1;
then O is open ;
hence ex b₁ being open Subset of (TOP-REAL n) ex e being Point of (Euclid n) st
( p = e & b₁ = OpenHypercube (e,r) ) ; :: thesis: verum