let n be Nat; :: thesis: for r being Real
for p, q being Point of (TOP-REAL n) st q in OpenHypercube (p,(r / 2)) holds
OpenHypercube (q,(r / 2)) c= OpenHypercube (p,r)
let r be Real; :: thesis: for p, q being Point of (TOP-REAL n) st q in OpenHypercube (p,(r / 2)) holds
OpenHypercube (q,(r / 2)) c= OpenHypercube (p,r)
let p, q be Point of (TOP-REAL n); :: thesis: ( q in OpenHypercube (p,(r / 2)) implies OpenHypercube (q,(r / 2)) c= OpenHypercube (p,r) )
assume A1: q in OpenHypercube (p,(r / 2)) ; :: thesis: OpenHypercube (q,(r / 2)) c= OpenHypercube (p,r)

now :: thesis: for x being object st x in OpenHypercube (q,(r / 2)) holds
x in OpenHypercube (p,r)

let x be object ; :: thesis: ( x in OpenHypercube (q,(r / 2)) implies x in OpenHypercube (p,r) )
assume A2: x in OpenHypercube (q,(r / 2)) ; :: thesis: x in OpenHypercube (p,r)
then reconsider x1 = x as Point of (TOP-REAL n) ;

now :: thesis: for i being Nat st i in Seg n holds
x1 . i in ].((p . i) - r),((p . i) + r).[

let i be Nat; :: thesis: ( i in Seg n implies x1 . i in ].((p . i) - r),((p . i) + r).[ )
assume A3: i in Seg n ; :: thesis: x1 . i in ].((p . i) - r),((p . i) + r).[
then x1 . i in ].((q . i) - (r / 2)),((q . i) + (r / 2)).[ by A2, TIETZE_2:4;
then A4: ( (q . i) - (r / 2) < x1 . i & x1 . i < (q . i) + (r / 2) ) by XXREAL_1:4;
q . i in ].((p . i) - (r / 2)),((p . i) + (r / 2)).[ by A1, A3, TIETZE_2:4;
then ( (p . i) - (r / 2) < q . i & q . i < (p . i) + (r / 2) ) by XXREAL_1:4;
then ( ((p . i) - (r / 2)) - (r / 2) < (q . i) - (r / 2) & (q . i) + (r / 2) < ((p . i) + (r / 2)) + (r / 2) ) by XREAL_1:8;
then ( (p . i) - r < x1 . i & x1 . i < (p . i) + r ) by A4, XXREAL_0:2;
hence x1 . i in ].((p . i) - r),((p . i) + r).[ by XXREAL_1:4; :: thesis: verum

end;

hence x in OpenHypercube (p,r) by TIETZE_2:4; :: thesis: verum

end;

hence OpenHypercube (q,(r / 2)) c= OpenHypercube (p,r) ; :: thesis: verum