:: deftheorem Def4 defines FTSL1 FINTOPO4:def 4 :
for n being Nat st n > 0 holds
FTSL1 n = RelStr(# (Seg n),(Nbdl1 n) #);