let n be Nat; 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; 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); 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)); LATTICE7:def 1 ( 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)))))
; 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 for x being object st x in dom (Intervals (e,r)) holds
y . x in (Intervals (e,r)) . xlet x be
object ;
( x in dom (Intervals (e,r)) implies y . x in (Intervals (e,r)) . x )assume A6:
x in dom (Intervals (e,r))
;
y . x in (Intervals (e,r)) . xthen 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;
verum end;
hence
y in OpenHypercube (e,r)
by A5, CARD_3:9; verum