let n be Nat; :: thesis: for r being real number
for e1, e being Point of (Euclid n) st n <> 0 & e1 in OpenHypercube e,r holds
r > (abs (e1 - e)) . (max_diff_index e1,e)
let r be real number ; :: thesis: for e1, e being Point of (Euclid n) st n <> 0 & e1 in OpenHypercube e,r holds
r > (abs (e1 - e)) . (max_diff_index e1,e)
let e1, e be Point of (Euclid n); :: thesis: ( n <> 0 & e1 in OpenHypercube e,r implies r > (abs (e1 - e)) . (max_diff_index e1,e) )
set d = max_diff_index e1,e;
(abs (e1 - e)) . (max_diff_index e1,e) = abs ((e1 - e) . (max_diff_index e1,e)) by VALUED_1:18;
hence ( n <> 0 & e1 in OpenHypercube e,r implies r > (abs (e1 - e)) . (max_diff_index e1,e) ) by Th14; :: thesis: verum