:: deftheorem Def3 defines Nbdl1 FINTOPO4:def 3 :
for n being Nat
for b₂ being Relation of (Seg n) holds
( b₂ = Nbdl1 n iff for i being Element of NAT st i in Seg n holds
Im (b₂,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))} );