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