let n be Nat; for b being Element of REAL n
for p being Point of (TOP-REAL n) ex a being Element of REAL n st
( a = p & ClosedHypercube (p,b) = ClosedHyperInterval ((a - b),(a + b)) )
let b be Element of REAL n; for p being Point of (TOP-REAL n) ex a being Element of REAL n st
( a = p & ClosedHypercube (p,b) = ClosedHyperInterval ((a - b),(a + b)) )
let p be Point of (TOP-REAL n); ex a being Element of REAL n st
( a = p & ClosedHypercube (p,b) = ClosedHyperInterval ((a - b),(a + b)) )
reconsider a = p as Element of REAL n by EUCLID:22;
take
a
; ( a = p & ClosedHypercube (p,b) = ClosedHyperInterval ((a - b),(a + b)) )
thus
a = p
; ClosedHypercube (p,b) = ClosedHyperInterval ((a - b),(a + b))
A1:
ClosedHypercube (p,b) c= ClosedHyperInterval ((a - b),(a + b))
ClosedHyperInterval ((a - b),(a + b)) c= ClosedHypercube (p,b)
hence
ClosedHypercube (p,b) = ClosedHyperInterval ((a - b),(a + b))
by A1; verum