set T = TOP-REAL 0;
TopStruct(# the carrier of (TOP-REAL 0), the topology of (TOP-REAL 0) #) = TopSpaceMetr (Euclid 0) by EUCLID:def 8;
then A1: [#] (TOP-REAL 0) = {(<*> REAL)} by FINSEQ_2:112;
card {(<*> REAL)} = 1 by CARD_1:50;
then ind ([#] (TOP-REAL 0)) < 1 by A1, TOPDIM_1:8;
hence ( TOP-REAL 0 is with_finite_small_inductive_dimension & ind (TOP-REAL 0) = 0 ) by A1, TOPDIM_1:def 4, NAT_1:26; :: thesis: verum