for L being non empty 1-sorted
for N being non empty NetStr over L
for i being Element of N holds the carrier of (N | i) = { y where y is Element of N : i <= y }