theorem Th11: :: YELLOW_6:11

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