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