:: deftheorem Def5 defines NatEmbSeq TRIANG_1:def 5 :
for b₁ being SetSequence holds
( b₁ = NatEmbSeq iff for n being Nat holds b₁ . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } );