let n be Nat; :: thesis: for A being Subset of (TOP-REAL n) st not A is boundary holds
ind A = n
let A be Subset of (TOP-REAL n); :: thesis: ( not A is boundary implies ind A = n )
set TR = TOP-REAL n;
set E = the empty Subset of (TOP-REAL n);
consider Ia being affinely-independent Subset of (TOP-REAL n) such that
( the empty Subset of (TOP-REAL n) c= Ia & Ia c= [#] (TOP-REAL n) ) and
A1: Affin Ia = Affin ([#] (TOP-REAL n)) by RLAFFIN1:60;
A2: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider IA = Ia as finite Subset of (Euclid n) by TOPMETR:12;
IA <> {} by A1;
then consider X being object such that
A3: X in IA by XBOOLE_0:def 1;
reconsider X = X as Point of (Euclid n) by A3;
reconsider x = X as Point of (TOP-REAL n) by A2, TOPMETR:12;
A4: dim (TOP-REAL n) = n by RLAFFIN3:4;
[#] (TOP-REAL n) c= Affin ([#] (TOP-REAL n)) by RLAFFIN1:49;
then card Ia = (dim (TOP-REAL n)) + 1 by A1, XBOOLE_0:def 10, RLAFFIN3:6;
then A5: ind (conv Ia) = n by A4, SIMPLEX2:25;
set d = diameter IA;
A6: ind (TOP-REAL n) = n by SIMPLEX2:26;
Ia c= conv Ia by RLAFFIN1:2;
then A7: conv Ia c= cl_Ball (X,(diameter IA)) by A3, SIMPLEX2:13;
assume not A is boundary ; :: thesis: ind A = n
then Int A <> {} by TOPS_1:48;
then consider y being object such that
A8: y in Int A by XBOOLE_0:def 1;
reconsider y = y as Point of (TOP-REAL n) by A8;
reconsider Y = y as Point of (Euclid n) by A2, TOPMETR:12;
consider r being Real such that
A9: r > 0 and
A10: Ball (Y,r) c= A by A8, GOBOARD6:5;
set r2 = r / 2;
A11: n in NAT by ORDINAL1:def 12;
A12: Ball (Y,r) = Ball (y,r) by TOPREAL9:13;
(diameter IA) + 0 < (diameter IA) + 1 by XREAL_1:6;
then A13: cl_Ball (x,(diameter IA)) c= Ball (x,((diameter IA) + 1)) by A11, JORDAN:21;
cl_Ball (X,(diameter IA)) = cl_Ball (x,(diameter IA)) by TOPREAL9:14;
then conv Ia c= Ball (x,((diameter IA) + 1)) by A13, A7;
then A14: n <= ind (Ball (x,((diameter IA) + 1))) by A5, TOPDIM_1:19;
diameter IA >= 0 by TBSP_1:21;
then A15: ( cl_Ball (x,((diameter IA) + 1)) is compact & not cl_Ball (x,((diameter IA) + 1)) is boundary ) by Lm2;
cl_Ball (y,(r / 2)) c= Ball (y,r) by A9, XREAL_1:216, A11, JORDAN:21;
then cl_Ball (y,(r / 2)) c= A by A10, A12;
then A16: ind (cl_Ball (y,(r / 2))) <= ind A by TOPDIM_1:19;
( cl_Ball (y,(r / 2)) is compact & not cl_Ball (y,(r / 2)) is boundary ) by A9, Lm2;
then ex h being Function of ((TOP-REAL n) | (cl_Ball (x,((diameter IA) + 1)))),((TOP-REAL n) | (cl_Ball (y,(r / 2)))) st
( h is being_homeomorphism & h .: (Fr (cl_Ball (x,((diameter IA) + 1)))) = Fr (cl_Ball (y,(r / 2))) ) by A15, BROUWER2:7;
then cl_Ball (x,((diameter IA) + 1)), cl_Ball (y,(r / 2)) are_homeomorphic by T_0TOPSP:def 1, METRIZTS:def 1;
then A17: ind (cl_Ball (x,((diameter IA) + 1))) = ind (cl_Ball (y,(r / 2))) by TOPDIM_1:27;
Ball (x,((diameter IA) + 1)) c= cl_Ball (x,((diameter IA) + 1)) by TOPREAL9:16;
then ind (Ball (x,((diameter IA) + 1))) <= ind (cl_Ball (x,((diameter IA) + 1))) by TOPDIM_1:19;
then n <= ind (cl_Ball (y,(r / 2))) by A17, A14, XXREAL_0:2;
then A18: n <= ind A by A16, XXREAL_0:2;
ind A <= ind (TOP-REAL n) by TOPDIM_1:20;
hence ind A = n by A6, XXREAL_0:1, A18; :: thesis: verum