let n be Nat; :: thesis:
let r be Real; :: thesis:
let p, q be Point of (TOP-REAL n); :: thesis:
assume A1: q in OpenHypercube (p,(r / 2)) ; :: thesis:
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A2: x in OpenHypercube (q,(r / 2)) ; :: thesis:
then reconsider x1 = x as Point of (TOP-REAL n) ;

now :: thesis:

let i be Nat; :: thesis:
assume A3: i in Seg n ; :: thesis:
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:

end;

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