let n be Nat; :: thesis: ind (TOP-REAL n) = n
set T = TOP-REAL n;
consider I being affinely-independent Subset of (TOP-REAL n) such that
A1: ( {} (TOP-REAL n) c= I & I c= [#] (TOP-REAL n) & Affin I = Affin ([#] (TOP-REAL n)) ) by RLAFFIN1:60;
[#] (TOP-REAL n) is Affine by RUSUB_4:22;
then ( dim (TOP-REAL n) = n & Affin ([#] (TOP-REAL n)) = [#] (TOP-REAL n) ) by RLAFFIN1:50, RLAFFIN3:4;
then card I = n + 1 by A1, RLAFFIN3:6;
then ind (conv I) = n by Th25;
then ( ind (TOP-REAL n) >= n & ind (TOP-REAL n) <= n ) by TOPDIM_1:20, TOPDIM_2:21;
hence ind (TOP-REAL n) = n by XXREAL_0:1; :: thesis: verum