theorem Th9: :: FINTOPO5:9

for n being non zero Nat
for jn, j, k being Nat
for p being Element of (FTSL1 n) st p = jn holds
( j in U_FT (p,k) iff ( j in Seg n & |.(jn - j).| <= k + 1 ) )