for S being non empty 1-sorted
for N being net of S
for X being set
for M being subnet of N st M = N " X holds
for i being Element of M holds M . i in X