:: deftheorem Def6 defines FTSC1 FINTOPO4:def 6 :
for n being Nat st n > 0 holds
FTSC1 n = RelStr(# (Seg n),(Nbdc1 n) #);