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;
A5: dom y = dom (Intervals e,r) by A1, A3, A4, 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