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 finite-ind & ind (TOP-REAL 0) = 0 ) by A1, NAT_1:25; :: thesis: verum