theorem Th12: :: YELLOW_6:12

for S being 1-sorted
for N being non empty NetStr over S
for M being non empty full SubNetStr of N
for x, y being Element of N
for i, j being Element of M st x = i & y = j & x <= y holds
i <= j