let n be Nat; :: thesis: for r being Real
for p, q being Point of (TOP-REAL n) st q in OpenHypercube (p,r) holds
p in OpenHypercube (q,r)
let r be Real; :: thesis: for p, q being Point of (TOP-REAL n) st q in OpenHypercube (p,r) holds
p in OpenHypercube (q,r)
let p, q be Point of (TOP-REAL n); :: thesis: ( q in OpenHypercube (p,r) implies p in OpenHypercube (q,r) )
assume A1: q in OpenHypercube (p,r) ; :: thesis: p in OpenHypercube (q,r)
now :: thesis: for i being Nat st i in Seg n holds
p . i in ].((q . i) - r),((q . i) + r).[
let i be Nat; :: thesis: ( i in Seg n implies p . i in ].((q . i) - r),((q . i) + r).[ )
assume i in Seg n ; :: thesis: p . i in ].((q . i) - r),((q . i) + r).[
then q . i in ].((p . i) - r),((p . i) + r).[ by A1, TIETZE_2:4;
then ( (p . i) - r < q . i & q . i < (p . i) + r ) by XXREAL_1:4;
then ( ((p . i) - r) + r < (q . i) + r & (q . i) - r < ((p . i) + r) - r ) by XREAL_1:8;
hence p . i in ].((q . i) - r),((q . i) + r).[ by XXREAL_1:4; :: thesis: verum
end;
hence p in OpenHypercube (q,r) by TIETZE_2:4; :: thesis: verum