set E = Euclid n;
set TE = TopSpaceMetr (Euclid n);
set TR = TOP-REAL n;
A1: the carrier of (TOP-REAL n) = the carrier of (Euclid n) by EUCLID:67;
A2: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider H = ClosedHypercube (p,R) as Subset of TopStruct(# the carrier of (TopSpaceMetr (Euclid n)), the topology of (TopSpaceMetr (Euclid n)) #) ;
A3: H ` = ([#] (TopSpaceMetr (Euclid n))) \ H by SUBSET_1:def 4;
for e being Point of (Euclid n) st e in H ` holds
ex r being Real st
( r > 0 & OpenHypercube (e,r) c= H ` )

proof

let e be Point of (Euclid n); :: thesis: ( e in H ` implies ex r being Real st
( r > 0 & OpenHypercube (e,r) c= H ` ) )
reconsider ee = e as Point of (TOP-REAL n) by EUCLID:67;
assume e in H ` ; :: thesis: ex r being Real st
( r > 0 & OpenHypercube (e,r) c= H ` )
then not e in H by A3, XBOOLE_0:def 5;
then consider i being Nat such that
A4: i in Seg n and
A5: not e . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] by A1, Def2;

per cases ( e . i < (p . i) - (R . i) or e . i > (p . i) + (R . i) ) by A5, XXREAL_1:1;

suppose A6: e . i < (p . i) - (R . i) ; :: thesis: ex r being Real st
( r > 0 & OpenHypercube (e,r) c= H ` )

take r = ((p . i) - (R . i)) - (e . i); :: thesis: ( r > 0 & OpenHypercube (e,r) c= H ` )
(e . i) - (e . i) < r by A6, XREAL_1:9;
hence r > 0 ; :: thesis: OpenHypercube (e,r) c= H `
set I = Intervals (e,r);
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in OpenHypercube (e,r) or x in H ` )
assume A7: x in OpenHypercube (e,r) ; :: thesis: x in H `
then A8: x in product (Intervals (e,r)) by EUCLID_9:def 4;
assume not x in H ` ; :: thesis: contradiction
then not x in ([#] (TopSpaceMetr (Euclid n))) \ H by SUBSET_1:def 4;
then A9: x in H by A7, XBOOLE_0:def 5;
reconsider x = x as Point of (Euclid n) by TOPMETR:12, A7;
reconsider xx = x as Point of (TOP-REAL n) by EUCLID:67;
len ee = n by CARD_1:def 7;
then A10: dom e = Seg n by FINSEQ_1:def 3;
dom e = dom (Intervals (e,r)) by EUCLID_9:def 3;
then x . i in (Intervals (e,r)) . i by A10, A4, A8, CARD_3:9;
then x . i in ].((e . i) - r),((e . i) + r).[ by A10, A4, EUCLID_9:def 3;
then A11: x . i < (p . i) - (R . i) by XXREAL_1:4;
xx . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] by A4, A9, Def2;
hence contradiction by A11, XXREAL_1:1; :: thesis: verum

end;

suppose A12: e . i > (p . i) + (R . i) ; :: thesis: ex r being Real st
( r > 0 & OpenHypercube (e,r) c= H ` )

take r = (e . i) - ((p . i) + (R . i)); :: thesis: ( r > 0 & OpenHypercube (e,r) c= H ` )
(e . i) - (e . i) < r by A12, XREAL_1:10;
hence r > 0 ; :: thesis: OpenHypercube (e,r) c= H `
set I = Intervals (e,r);
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in OpenHypercube (e,r) or x in H ` )
assume A13: x in OpenHypercube (e,r) ; :: thesis: x in H `
then A14: x in product (Intervals (e,r)) by EUCLID_9:def 4;
assume not x in H ` ; :: thesis: contradiction
then not x in ([#] (TopSpaceMetr (Euclid n))) \ H by SUBSET_1:def 4;
then A15: x in H by A13, XBOOLE_0:def 5;
reconsider x = x as Point of (Euclid n) by TOPMETR:12, A13;
reconsider xx = x as Point of (TOP-REAL n) by EUCLID:67;
len ee = n by CARD_1:def 7;
then A16: dom e = Seg n by FINSEQ_1:def 3;
dom e = dom (Intervals (e,r)) by EUCLID_9:def 3;
then x . i in (Intervals (e,r)) . i by A16, A4, A14, CARD_3:9;
then x . i in ].((e . i) - r),((e . i) + r).[ by A16, A4, EUCLID_9:def 3;
then A17: x . i > (p . i) + (R . i) by XXREAL_1:4;
xx . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] by A4, A15, Def2;
hence contradiction by A17, XXREAL_1:1; :: thesis: verum

end;

end;

end;

then H ` is open by EUCLID_9:24;
then (ClosedHypercube (p,R)) ` is open by A2;
then A18: ClosedHypercube (p,R) is closed by TOPS_1:3;
reconsider h = H as Subset of (Euclid n) by EUCLID:67;
reconsider P = p as Point of (Euclid n) by EUCLID:67;
ClosedHypercube (p,R) is convex

proof

let u, w be Point of (TOP-REAL n); :: according to CONVEX1:def 2 :: thesis: for b₁ being object holds
( b₁ <= 0 or 1 <= b₁ or not u in ClosedHypercube (p,R) or not w in ClosedHypercube (p,R) or K181((TOP-REAL n),(b₁ * u),((1 - b₁) * w)) in ClosedHypercube (p,R) )
let r be Real; :: thesis: ( r <= 0 or 1 <= r or not u in ClosedHypercube (p,R) or not w in ClosedHypercube (p,R) or K181((TOP-REAL n),(r * u),((1 - r) * w)) in ClosedHypercube (p,R) )
assume that
A19: 0 < r and
A20: r < 1 and
A21: u in ClosedHypercube (p,R) and
A22: w in ClosedHypercube (p,R) ; :: thesis: K181((TOP-REAL n),(r * u),((1 - r) * w)) in ClosedHypercube (p,R)
set ru = r * u;
set rw = (1 - r) * w;
A23: 1 - r > 1 - 1 by A20, XREAL_1:10;

now :: thesis: for i being Nat st i in Seg n holds
((r * u) + ((1 - r) * w)) . i in [.((p . i) - (R . i)),((p . i) + (R . i)).]

let i be Nat; :: thesis: ( i in Seg n implies ((r * u) + ((1 - r) * w)) . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] )
A24: len ((1 - r) * w) = n by CARD_1:def 7;
assume A25: i in Seg n ; :: thesis: ((r * u) + ((1 - r) * w)) . i in [.((p . i) - (R . i)),((p . i) + (R . i)).]
then A26: u . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] by A21, Def2;
then u . i >= (p . i) - (R . i) by XXREAL_1:1;
then A27: r * (u . i) >= r * ((p . i) - (R . i)) by A19, XREAL_1:64;
len (r * u) = n by CARD_1:def 7;
then dom (r * u) = dom ((1 - r) * w) by A24, FINSEQ_3:29;
then i in (dom (r * u)) /\ (dom ((1 - r) * w)) by A24, FINSEQ_1:def 3, A25;
then i in dom ((r * u) + ((1 - r) * w)) by VALUED_1:def 1;
then A28: ((r * u) + ((1 - r) * w)) . i = ((r * u) . i) + (((1 - r) * w) . i) by VALUED_1:def 1;
u . i <= (p . i) + (R . i) by A26, XXREAL_1:1;
then A29: r * (u . i) <= r * ((p . i) + (R . i)) by A19, XREAL_1:64;
A30: (r * u) . i = r * (u . i) by VALUED_1:6;
A31: ((1 - r) * w) . i = (1 - r) * (w . i) by VALUED_1:6;
A32: w . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] by A25, A22, Def2;
then w . i <= (p . i) + (R . i) by XXREAL_1:1;
then (1 - r) * (w . i) <= (1 - r) * ((p . i) + (R . i)) by A23, XREAL_1:64;
then A33: ((r * u) + ((1 - r) * w)) . i <= (r * ((p . i) + (R . i))) + ((1 - r) * ((p . i) + (R . i))) by A29, A30, A31, A28, XREAL_1:7;
w . i >= (p . i) - (R . i) by A32, XXREAL_1:1;
then (1 - r) * (w . i) >= (1 - r) * ((p . i) - (R . i)) by A23, XREAL_1:64;
then ((r * u) + ((1 - r) * w)) . i >= (r * ((p . i) - (R . i))) + ((1 - r) * ((p . i) - (R . i))) by A27, A30, A31, A28, XREAL_1:7;
hence ((r * u) + ((1 - r) * w)) . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] by A33, XXREAL_1:1; :: thesis: verum

end;

hence K181((TOP-REAL n),(r * u),((1 - r) * w)) in ClosedHypercube (p,R) by Def2; :: thesis: verum

end;

hence ClosedHypercube (p,R) is convex ; :: thesis: ClosedHypercube (p,R) is compact

per cases ( R .: (Seg n) is empty or not R .: (Seg n) is empty ) ;

suppose A34: R .: (Seg n) is empty ; :: thesis: ClosedHypercube (p,R) is compact

H c= {p}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H or x in {p} )
A35: len p = n by CARD_1:def 7;
assume A36: x in H ; :: thesis: x in {p}
then reconsider x = x as Point of (TOP-REAL n) ;

A37: now :: thesis: for i being Nat st 1 <= i & i <= n holds
x . i = p . i

let i be Nat; :: thesis: ( 1 <= i & i <= n implies x . i = p . i )
assume that
A38: 1 <= i and
A39: i <= n ; :: thesis: x . i = p . i
A40: i in Seg n by A38, A39, FINSEQ_1:1;
not R . i in R .: (Seg n) by A34;
then not i in dom R by A40, FUNCT_1:def 6;
then A41: R . i = 0 by FUNCT_1:def 2;
x . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] by A40, A36, Def2;
then x . i in {(p . i)} by A41, XXREAL_1:17;
hence x . i = p . i by TARSKI:def 1; :: thesis: verum

end;

len x = n by CARD_1:def 7;
then x = p by A35, A37, FINSEQ_1:14;
hence x in {p} by TARSKI:def 1; :: thesis: verum

end;

then h is bounded ;
then ClosedHypercube (p,R) is bounded by JORDAN2C:11;
hence ClosedHypercube (p,R) is compact by A18; :: thesis: verum

end;

suppose A42: not R .: (Seg n) is empty ; :: thesis: ClosedHypercube (p,R) is compact

then reconsider RS = R .: (Seg n) as real-membered right_end set ;
set m = (max RS) + 1;
set O = OpenHypercube (P,((max RS) + 1));
set I = Intervals (P,((max RS) + 1));
A43: H c= OpenHypercube (P,((max RS) + 1))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H or x in OpenHypercube (P,((max RS) + 1)) )
A44: dom (Intervals (P,((max RS) + 1))) = dom P by EUCLID_9:def 3;
assume A45: x in H ; :: thesis: x in OpenHypercube (P,((max RS) + 1))
then reconsider x = x as Point of (TOP-REAL n) ;
A46: len x = n by CARD_1:def 7;
len p = n by CARD_1:def 7;
then A47: dom x = dom p by A46, FINSEQ_3:29;
A48: dom x = Seg n by A46, FINSEQ_1:def 3;
for z being object st z in dom (Intervals (P,((max RS) + 1))) holds
x . z in (Intervals (P,((max RS) + 1))) . z

proof

let z be object ; :: thesis: ( z in dom (Intervals (P,((max RS) + 1))) implies x . z in (Intervals (P,((max RS) + 1))) . z )
assume A49: z in dom (Intervals (P,((max RS) + 1))) ; :: thesis: x . z in (Intervals (P,((max RS) + 1))) . z
then A50: x . z in [.((P . z) - (R . z)),((p . z) + (R . z)).] by A45, A47, A48, A44, Def2;
then A51: (P . z) - (R . z) <= x . z by XXREAL_1:1;

A52: now :: thesis: R . z < (max RS) + 1

per cases ( z in dom R or not z in dom R ) ;

suppose z in dom R ; :: thesis: R . z < (max RS) + 1

then R . z in RS by A49, A47, A48, A44, FUNCT_1:def 6;
then R . z <= max RS by XXREAL_2:def 8;
then (R . z) + 0 < (max RS) + 1 by XREAL_1:8;
hence R . z < (max RS) + 1 ; :: thesis: verum

end;

suppose A53: not z in dom R ; :: thesis: R . z < (max RS) + 1

Seg n meets dom R by A42, RELAT_1:118;
then consider i being object such that
A54: i in Seg n and
A55: i in dom R by XBOOLE_0:3;
reconsider i = i as Nat by A54;
i in (Seg n) /\ (dom R) by A54, A55, XBOOLE_0:def 4;
then A56: R . i >= 0 by Th4, A45;
R . i in RS by A54, A55, FUNCT_1:def 6;
then R . i <= max RS by XXREAL_2:def 8;
then 0 + 0 < (max RS) + 1 by A56;
hence R . z < (max RS) + 1 by A53, FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

then (P . z) - ((max RS) + 1) < (P . z) - (R . z) by XREAL_1:10;
then A57: (P . z) - ((max RS) + 1) < x . z by A51, XXREAL_0:2;
A58: x . z <= (p . z) + (R . z) by A50, XXREAL_1:1;
(P . z) + ((max RS) + 1) > (P . z) + (R . z) by A52, XREAL_1:8;
then A59: x . z < (P . z) + ((max RS) + 1) by A58, XXREAL_0:2;
(Intervals (P,((max RS) + 1))) . z = ].((P . z) - ((max RS) + 1)),((P . z) + ((max RS) + 1)).[ by A49, A44, EUCLID_9:def 3;
hence x . z in (Intervals (P,((max RS) + 1))) . z by A57, A59, XXREAL_1:4; :: thesis: verum

end;

then x in product (Intervals (P,((max RS) + 1))) by A47, A44, CARD_3:9;
hence x in OpenHypercube (P,((max RS) + 1)) by EUCLID_9:def 4; :: thesis: verum

end;

n <> 0 by A42;
then OpenHypercube (P,((max RS) + 1)) c= Ball (P,(((max RS) + 1) * (sqrt n))) by EUCLID_9:18;
then h is bounded by A43, XBOOLE_1:1, TBSP_1:14;
then ClosedHypercube (p,R) is bounded by JORDAN2C:11;
hence ClosedHypercube (p,R) is compact by A18; :: thesis: verum

end;

end;