let n be Nat; :: thesis: for r being Real
for e being Point of (Euclid n) holds Ball (e,r) c= OpenHypercube (e,r)
let r be Real; :: thesis: for e being Point of (Euclid n) holds Ball (e,r) c= OpenHypercube (e,r)
let e be Point of (Euclid n); :: thesis: Ball (e,r) c= OpenHypercube (e,r)
let g be object ; :: according to TARSKI:def 3 :: thesis: ( not g in Ball (e,r) or g in OpenHypercube (e,r) )
assume A1: g in Ball (e,r) ; :: thesis: g in OpenHypercube (e,r)
then reconsider g = g as Point of (Euclid n) ;
A2: dom (Intervals (e,r)) = dom e by Def3;
A3: ( dom g = Seg n & dom e = Seg n ) by FINSEQ_1:89;
now :: thesis: for x being object st x in dom (Intervals (e,r)) holds
g . x in (Intervals (e,r)) . x
let x be object ; :: thesis: ( x in dom (Intervals (e,r)) implies g . x in (Intervals (e,r)) . x )
reconsider u = e . x, v = g . x as Real ;
assume A4: x in dom (Intervals (e,r)) ; :: thesis: g . x in (Intervals (e,r)) . x
then A5: (Intervals (e,r)) . x = ].(u - r),(u + r).[ by A2, Def3;
dom (g - e) = (dom g) /\ (dom e) by VALUED_1:12;
then A6: (g - e) . x = v - u by A2, A3, A4, VALUED_1:13;
A7: v = u + (v - u) ;
|.((g - e) . x).| < r by A1, Th10;
hence g . x in (Intervals (e,r)) . x by A6, A5, A7, FCONT_3:3; :: thesis: verum
end;
hence g in OpenHypercube (e,r) by A2, A3, CARD_3:9; :: thesis: verum