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

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