let n be Nat; :: thesis: for A being Subset of () st not A is boundary holds
ind A = n

let A be Subset of (); :: thesis: ( not A is boundary implies ind A = n )
set TR = TOP-REAL n;
set E = the empty Subset of ();
consider Ia being affinely-independent Subset of () such that
( the empty Subset of () c= Ia & Ia c= [#] () ) and
A1: Affin Ia = Affin ([#] ()) by RLAFFIN1:60;
A2: TopStruct(# the carrier of (), the topology of () #) = TopSpaceMetr () by EUCLID:def 8;
then reconsider IA = Ia as finite Subset of () 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 () by A3;
reconsider x = X as Point of () by ;
A4: dim () = n by RLAFFIN3:4;
[#] () c= Affin ([#] ()) by RLAFFIN1:49;
then card Ia = (dim ()) + 1 by ;
then A5: ind (conv Ia) = n by ;
set d = diameter IA;
A6: ind () = n by SIMPLEX2:26;
Ia c= conv Ia by RLAFFIN1:2;
then A7: conv Ia c= cl_Ball (X,(diameter IA)) by ;
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 () by A8;
reconsider Y = y as Point of () by ;
consider r being Real such that
A9: r > 0 and
A10: Ball (Y,r) c= A by ;
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 ;
cl_Ball (X,(diameter IA)) = cl_Ball (x,(diameter IA)) by TOPREAL9:14;
then conv Ia c= Ball (x,((diameter IA) + 1)) by ;
then A14: n <= ind (Ball (x,((diameter IA) + 1))) by ;
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 ;
then cl_Ball (y,(r / 2)) c= A by ;
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 ;
then ex h being Function of (() | (cl_Ball (x,((diameter IA) + 1)))),(() | (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 ;
then cl_Ball (x,((diameter IA) + 1)), cl_Ball (y,(r / 2)) are_homeomorphic by ;
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 ;
then A18: n <= ind A by ;
ind A <= ind () by TOPDIM_1:20;
hence ind A = n by ; :: thesis: verum