:: deftheorem defines FTSL2 FINTOPO5:def 3 :
for n, m being Nat holds FTSL2 (n,m) = RelStr(# [:(Seg n),(Seg m):],(Nbdl2 (n,m)) #);