:: deftheorem Def5 defines Nbdc1 FINTOPO4:def 5 :
for n being Nat
for b₂ being Relation of (Seg n) holds
( b₂ = Nbdc1 n iff for i being Element of NAT st i in Seg n holds
( ( 1 < i & i < n implies Im (b₂,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (b₂,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (b₂,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (b₂,i) = {i} ) ) );