let n be Nat; :: thesis: for r being Real
for e, e1 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; :: thesis: for e, e1 being Point of (Euclid n) holds OpenHypercube (e1,(r - ((abs (e1 - e)) . (max_diff_index (e1,e))))) c= OpenHypercube (e,r)
let e, e1 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 FINSEQ_1:89;
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:9;
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 :: thesis: for x being object st x in dom (Intervals (e,r)) holds
y . x in (Intervals (e,r)) . x

let x be object ; :: 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:9;
then A9: |.((y . x) - (e1 . x)).| < r - ((abs (e1 - e)) . (max_diff_index (e1,e))) by A8, RCOMP_1:1;
dom (e1 - e) = (dom e1) /\ (dom e) by VALUED_1:12;
then |.((e1 . x) - (e . x)).| = |.((e1 - e) . x).| by A1, A3, A4, A5, A6, VALUED_1:13
.= (abs (e1 - e)) . x by VALUED_1:18 ;
then A10: |.((y . x) - (e1 . x)).| + |.((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:8;
|.((y . x) - (e . x)).| <= |.((y . x) - (e1 . x)).| + |.((e1 . x) - (e . x)).| by COMPLEX1:63;
then |.((y . x) - (e . x)).| < r by A10, XXREAL_0:2;
hence y . x in (Intervals (e,r)) . x by A7, RCOMP_1:1; :: thesis: verum

end;

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