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:94;
card {(<*> REAL)} = 1 by CARD_1:30;
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, NAT_1:25, TOPDIM_1:def 4; :: thesis: verum