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

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