:: deftheorem Def2 defines Nbdl2 FINTOPO5:def 2 :
for n, m being Nat
for b₃ being Relation of [:(Seg n),(Seg m):] holds
( b₃ = Nbdl2 (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) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] );