:: deftheorem defines FTSS2 FINTOPO5:def 5 :
for n, m being Nat holds FTSS2 (n,m) = RelStr(# [:(Seg n),(Seg m):],(Nbds2 (n,m)) #);