:: deftheorem Def4 defines Nbds2 FINTOPO5:def 4 :
for n, m being Nat
for b₃ being Relation of [:(Seg n),(Seg m):] holds
( b₃ = Nbds2 (n,m) iff for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Nat st x = [i,j] holds
Im (b₃,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:] );