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 number 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 number st
( s > 0 & Ball p,s c= OpenHypercube e,r ) )
assume A2: p in OpenHypercube e,r ; :: thesis: ex s being real number 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:10;
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, XBOOLE_1:1; :: thesis: verum

end;

hence OpenHypercube e,r is open by TOPMETR:22; :: 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 5; :: thesis: verum

end;

end;