let n be Nat; :: thesis:
let p, q be Point of (TOP-REAL n); :: thesis:
let R be real-valued FinSequence; :: thesis:
set TR = TOP-REAL n;
A1: Fr (ClosedHypercube (p,R)) c= ClosedHypercube (p,R) by TOPS_1:35;
thus ( q in Fr (ClosedHypercube (p,R)) implies ( q in ClosedHypercube (p,R) & ex i being Nat st
( i in Seg n & ( q . i = (p . i) - (R . i) or q . i = (p . i) + (R . i) ) ) ) ) :: thesis:

deffunc H₁( set ) -> set = (q . $1) - ((p . $1) - (R . $1));
deffunc H₂( set ) -> set = ((p . $1) + (R . $1)) - (q . $1);
consider L1 being FinSequence such that
A2: ( len L1 = n & ( for i being Nat st i in dom L1 holds
L1 . i = H₁(i) ) ) from FINSEQ_1:sch 2();

let y be object ; :: thesis:
assume y in rng L1 ; :: thesis:
then consider x being object such that
A3: x in dom L1 and
A4: L1 . x = y by FUNCT_1:def 3;
reconsider x = x as Nat by A3;
L1 . x = H₁(x) by A2, A3;
hence y is real by A4; :: thesis:

end;

then A5: rng L1 is real-membered by MEMBERED:def 3;
consider R1 being FinSequence such that
A6: ( len R1 = n & ( for i being Nat st i in dom R1 holds
R1 . i = H₂(i) ) ) from FINSEQ_1:sch 2();

now :: thesis:

let y be object ; :: thesis:
assume y in rng R1 ; :: thesis:
then consider x being object such that
A7: x in dom R1 and
A8: R1 . x = y by FUNCT_1:def 3;
reconsider x = x as Nat by A7;
R1 . x = H₂(x) by A7, A6;
hence y is real by A8; :: thesis:

end;

then A9: rng R1 is real-membered by MEMBERED:def 3;
A10: dom L1 = Seg n by A2, FINSEQ_1:def 3;
assume A11: q in Fr (ClosedHypercube (p,R)) ; :: thesis:
hence q in ClosedHypercube (p,R) by A1; :: thesis:
assume A12: for i being Nat st i in Seg n holds
( q . i <> (p . i) - (R . i) & q . i <> (p . i) + (R . i) ) ; :: thesis:
n > 0

proof

assume n <= 0 ; :: thesis:
then n = 0 ;
then A13: {(0. (TOP-REAL n))} = the carrier of (TOP-REAL n) by EUCLID:22, JORDAN2C:105;
[#] (TOP-REAL n) is open ;
hence contradiction by A13, A11, ZFMISC_1:33; :: thesis:

end;

then n in Seg n by FINSEQ_1:3;
then L1 . n in rng L1 by A10, FUNCT_1:def 3;
then reconsider D = (rng L1) \/ (rng R1) as non empty finite real-membered set by A9, A5;
set m = min D;
consider e being Point of (Euclid n) such that
A14: q = e and
A15: OpenHypercube (q,(min D)) = OpenHypercube (e,(min D)) by Def1;
A16: dom R1 = Seg n by A6, FINSEQ_1:def 3;
A17: min D in D by XXREAL_2:def 7;
A18: min D > 0

proof

per cases by A17, XBOOLE_0:def 3;

suppose min D in rng L1 ; :: thesis:

then consider x being object such that
A19: x in dom L1 and
A20: L1 . x = min D by FUNCT_1:def 3;
reconsider x = x as Nat by A19;
q . x in [.((p . x) - (R . x)),((p . x) + (R . x)).] by A11, A1, A19, A10, Def2;
then q . x >= (p . x) - (R . x) by XXREAL_1:1;
then A21: q . x > (p . x) - (R . x) by A19, A10, A12, XXREAL_0:1;
L1 . x = H₁(x) by A2, A19;
hence min D > 0 by A21, XREAL_1:50, A20; :: thesis:

end;

suppose min D in rng R1 ; :: thesis:

then consider x being object such that
A22: x in dom R1 and
A23: R1 . x = min D by FUNCT_1:def 3;
reconsider x = x as Nat by A22;
q . x in [.((p . x) - (R . x)),((p . x) + (R . x)).] by A11, A1, A22, A16, Def2;
then q . x <= (p . x) + (R . x) by XXREAL_1:1;
then A24: q . x < (p . x) + (R . x) by A22, A16, A12, XXREAL_0:1;
R1 . x = H₂(x) by A6, A22;
hence min D > 0 by A24, XREAL_1:50, A23; :: thesis:

end;

set O = OpenHypercube (e,(min D));
OpenHypercube (e,(min D)) c= ClosedHypercube (p,R)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A25: x in OpenHypercube (e,(min D)) ; :: thesis:
then reconsider w = x as Point of (Euclid n) by TOPMETR:12;
reconsider W = w as Point of (TOP-REAL n) by EUCLID:67;
for i being Nat st i in Seg n holds
W . i in [.((p . i) - (R . i)),((p . i) + (R . i)).]

proof

let i be Nat; :: thesis:
set P = PROJ (n,i);
len W = n by CARD_1:def 7;
then A26: dom W = Seg n by FINSEQ_1:def 3;
dom (PROJ (n,i)) = the carrier of (TOP-REAL n) by FUNCT_2:def 1;
then A27: (PROJ (n,i)) . W in (PROJ (n,i)) .: (OpenHypercube (e,(min D))) by A25, FUNCT_1:def 6;
assume A28: i in Seg n ; :: thesis:
then L1 . i in rng L1 by A10, FUNCT_1:def 3;
then A29: L1 . i in D by XBOOLE_0:def 3;
L1 . i = H₁(i) by A10, A2, A28;
then min D <= H₁(i) by A29, XXREAL_2:def 7;
then A30: (q . i) - (min D) >= (q . i) - H₁(i) by XREAL_1:10;
(PROJ (n,i)) . W = W /. i by TOPREALC:def 6
.= W . i by A28, A26, PARTFUN1:def 6 ;
then A31: W . i in ].((e . i) - (min D)),((e . i) + (min D)).[ by A14, A15, A28, Th2, A27;
then W . i > (q . i) - (min D) by A14, XXREAL_1:4;
then A32: W . i > (p . i) - (R . i) by A30, XXREAL_0:2;
R1 . i in rng R1 by A28, A16, FUNCT_1:def 3;
then A33: R1 . i in D by XBOOLE_0:def 3;
R1 . i = H₂(i) by A16, A6, A28;
then min D <= H₂(i) by A33, XXREAL_2:def 7;
then A34: (q . i) + (min D) <= (q . i) + H₂(i) by XREAL_1:6;
W . i < (q . i) + (min D) by A31, A14, XXREAL_1:4;
then W . i < (p . i) + (R . i) by A34, XXREAL_0:2;
hence W . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] by A32, XXREAL_1:1; :: thesis:

end;

hence x in ClosedHypercube (p,R) by Def2; :: thesis:

end;

then q in Int (ClosedHypercube (p,R)) by A18, A14, A15, EUCLID_9:11, TOPS_1:22;
hence contradiction by TOPS_1:39, A11, XBOOLE_0:3; :: thesis:

end;

assume A35: q in ClosedHypercube (p,R) ; :: thesis:
given i being Nat such that A36: i in Seg n and
A37: ( q . i = (p . i) - (R . i) or q . i = (p . i) + (R . i) ) ; :: thesis:
for S being Subset of (TOP-REAL n) st S is open & q in S holds
( ClosedHypercube (p,R) meets S & (ClosedHypercube (p,R)) ` meets S )

proof

let S be Subset of (TOP-REAL n); :: thesis:
reconsider Q = q as Point of (Euclid n) by EUCLID:67;
assume that
A38: S is open and
A39: q in S ; :: thesis:
thus ClosedHypercube (p,R) meets S by A39, A35, XBOOLE_0:3; :: thesis:
Int S = S by A38, TOPS_1:23;
then consider s being Real such that
A40: s > 0 and
A41: Ball (Q,s) c= S by A39, GOBOARD6:5;
set s2 = s / 2;
A42: ( 0 < s / 2 & s / 2 < s ) by XREAL_1:216, A40;
A43: Ball (Q,s) = Ball (q,s) by TOPREAL9:13;

per cases by A37;

suppose A44: q . i = (p . i) - (R . i) ; :: thesis:

set q1 = q +* (i,((q . i) - (s / 2)));
reconsider q1 = q +* (i,((q . i) - (s / 2))) as Point of (TOP-REAL n) ;
len q = n by CARD_1:def 7;
then dom q = Seg n by FINSEQ_1:def 3;
then q1 . i = (q . i) - (s / 2) by A36, FUNCT_7:31;
then q1 . i < (q . i) + 0 by A40, XREAL_1:6;
then not q1 . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] by A44, XXREAL_1:1;
then not q1 in ClosedHypercube (p,R) by A36, Def2;
then q1 in ([#] (TOP-REAL n)) \ (ClosedHypercube (p,R)) by XBOOLE_0:def 5;
then A45: q1 in (ClosedHypercube (p,R)) ` by SUBSET_1:def 4;
q1 - q = (0* n) +* (i,(((q . i) - (s / 2)) - (q . i))) by TOPREALC:17;
then |.(q1 - q).| = |.(((q . i) - (s / 2)) - (q . i)).| by A36, TOPREALC:13
.= - (- (s / 2)) by A40, ABSVALUE:def 1
.= s / 2 ;
then q1 in Ball (q,s) by A42;
hence (ClosedHypercube (p,R)) ` meets S by A43, A41, XBOOLE_0:3, A45; :: thesis:

end;

suppose A46: q . i = (p . i) + (R . i) ; :: thesis:

set q1 = q +* (i,((q . i) + (s / 2)));
reconsider q1 = q +* (i,((q . i) + (s / 2))) as Point of (TOP-REAL n) ;
len q = n by CARD_1:def 7;
then dom q = Seg n by FINSEQ_1:def 3;
then q1 . i = (q . i) + (s / 2) by A36, FUNCT_7:31;
then q1 . i > (q . i) + 0 by A40, XREAL_1:6;
then not q1 . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] by A46, XXREAL_1:1;
then not q1 in ClosedHypercube (p,R) by A36, Def2;
then q1 in ([#] (TOP-REAL n)) \ (ClosedHypercube (p,R)) by XBOOLE_0:def 5;
then A47: q1 in (ClosedHypercube (p,R)) ` by SUBSET_1:def 4;
q1 - q = (0* n) +* (i,(((q . i) + (s / 2)) - (q . i))) by TOPREALC:17;
then |.(q1 - q).| = |.(((q . i) + (s / 2)) - (q . i)).| by A36, TOPREALC:13
.= s / 2 by A40, ABSVALUE:def 1 ;
then q1 in Ball (q,s) by A42;
hence (ClosedHypercube (p,R)) ` meets S by A43, A41, XBOOLE_0:3, A47; :: thesis:

end;

hence q in Fr (ClosedHypercube (p,R)) by TOPS_1:28; :: thesis: