theorem Th13: :: WAYBEL_9:13

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) c= the carrier of N