per cases ( n <> 0 or n = 0 ) ;

suppose A1: n <> 0 ; :: thesis: OpenHypercube (e,r) is open

for p being Point of (Euclid n) st p in OpenHypercube (e,r) holds
ex s being Real st
( s > 0 & Ball (p,s) c= OpenHypercube (e,r) )

proof

let p be Point of (Euclid n); :: thesis: ( p in OpenHypercube (e,r) implies ex s being Real st
( s > 0 & Ball (p,s) c= OpenHypercube (e,r) ) )
assume A2: p in OpenHypercube (e,r) ; :: thesis: ex s being Real st
( s > 0 & Ball (p,s) c= OpenHypercube (e,r) )
set d = (abs (p - e)) . (max_diff_index (p,e));
take s = r - ((abs (p - e)) . (max_diff_index (p,e))); :: thesis: ( s > 0 & Ball (p,s) c= OpenHypercube (e,r) )
r - ((abs (p - e)) . (max_diff_index (p,e))) > ((abs (p - e)) . (max_diff_index (p,e))) - ((abs (p - e)) . (max_diff_index (p,e))) by A1, A2, Th20, XREAL_1:8;
hence s > 0 ; :: thesis: Ball (p,s) c= OpenHypercube (e,r)
A3: OpenHypercube (p,s) c= OpenHypercube (e,r) by Th21;
Ball (p,s) c= OpenHypercube (p,s) by Th22;
hence Ball (p,s) c= OpenHypercube (e,r) by A3; :: thesis: verum

end;

hence OpenHypercube (e,r) is open by TOPMETR:15; :: thesis: verum

end;

suppose A4: n = 0 ; :: thesis: OpenHypercube (e,r) is open

then OpenHypercube (e,r) = {{}} by Th12;
then OpenHypercube (e,r) in the topology of (TopSpaceMetr (Euclid 0)) by Th6, TARSKI:def 2;
hence OpenHypercube (e,r) is open by A4, PRE_TOPC:def 2; :: thesis: verum

end;

end;