let n be Nat; :: thesis: for r being real number
for e1, e being Point of (Euclid n) holds OpenHypercube (e1,(r - ((abs (e1 - e)) . (max_diff_index (e1,e))))) c= OpenHypercube (e,r)
let r be real number ; :: thesis: for e1, e being Point of (Euclid n) holds OpenHypercube (e1,(r - ((abs (e1 - e)) . (max_diff_index (e1,e))))) c= OpenHypercube (e,r)
let e1, e be Point of (Euclid n); :: thesis: OpenHypercube (e1,(r - ((abs (e1 - e)) . (max_diff_index (e1,e))))) c= OpenHypercube (e,r)
set d = max_diff_index (e1,e);
set F = abs (e1 - e);
set s = r - ((abs (e1 - e)) . (max_diff_index (e1,e)));
A1: ( dom e1 = Seg n & dom e = Seg n ) by EUCLID:3;
let y be Point of (TopSpaceMetr (Euclid n)); :: according to LATTICE7:def 1 :: thesis: ( not y in OpenHypercube (e1,(r - ((abs (e1 - e)) . (max_diff_index (e1,e))))) or y in OpenHypercube (e,r) )
assume A2: y in OpenHypercube (e1,(r - ((abs (e1 - e)) . (max_diff_index (e1,e))))) ; :: thesis: y in OpenHypercube (e,r)
reconsider y = y as Point of (Euclid n) ;
A3: dom y = dom (Intervals (e1,(r - ((abs (e1 - e)) . (max_diff_index (e1,e)))))) by A2, CARD_3:18;
A4: dom (Intervals (e1,(r - ((abs (e1 - e)) . (max_diff_index (e1,e)))))) = dom e1 by Def3;
then A5: dom y = dom (Intervals (e,r)) by A1, A3, Def3;

now

let x be set ; :: thesis: ( x in dom (Intervals (e,r)) implies y . x in (Intervals (e,r)) . x )
assume A6: x in dom (Intervals (e,r)) ; :: thesis: y . x in (Intervals (e,r)) . x
then A7: (Intervals (e,r)) . x = ].((e . x) - r),((e . x) + r).[ by A1, A3, A4, A5, Def3;
A8: (Intervals (e1,(r - ((abs (e1 - e)) . (max_diff_index (e1,e)))))) . x = ].((e1 . x) - (r - ((abs (e1 - e)) . (max_diff_index (e1,e))))),((e1 . x) + (r - ((abs (e1 - e)) . (max_diff_index (e1,e))))).[ by A3, A4, A5, A6, Def3;
y . x in (Intervals (e1,(r - ((abs (e1 - e)) . (max_diff_index (e1,e)))))) . x by A2, A3, A5, A6, CARD_3:18;
then A9: abs ((y . x) - (e1 . x)) < r - ((abs (e1 - e)) . (max_diff_index (e1,e))) by A8, RCOMP_1:8;
dom (e1 - e) = (dom e1) /\ (dom e) by VALUED_1:12;
then abs ((e1 . x) - (e . x)) = abs ((e1 - e) . x) by A1, A3, A4, A5, A6, VALUED_1:13
.= (abs (e1 - e)) . x by VALUED_1:18 ;
then A10: (abs ((y . x) - (e1 . x))) + (abs ((e1 . x) - (e . x))) < (r - ((abs (e1 - e)) . (max_diff_index (e1,e)))) + ((abs (e1 - e)) . (max_diff_index (e1,e))) by A9, Th5, XREAL_1:10;
abs ((y . x) - (e . x)) <= (abs ((y . x) - (e1 . x))) + (abs ((e1 . x) - (e . x))) by COMPLEX1:149;
then abs ((y . x) - (e . x)) < r by A10, XXREAL_0:2;
hence y . x in (Intervals (e,r)) . x by A7, RCOMP_1:8; :: thesis: verum

end;

hence y in OpenHypercube (e,r) by A5, CARD_3:18; :: thesis: verum