theorem Th17: :: WAYBEL_9:17

for L being non empty 1-sorted
for N being net of L
for i being Element of N holds N | i is subnet of N