let n be Nat; :: thesis: for r being Real
for e, e1 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; :: thesis: for e, e1 being Point of (Euclid n) st n <> 0 & e1 in OpenHypercube (e,r) holds
r > (abs (e1 - e)) . (max_diff_index (e1,e))
let e, e1 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)) = |.((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