:: deftheorem Def9 defines subnet YELLOW_6:def 9 :
for T being non empty 1-sorted
for N, b₃ being net of T holds
( b₃ is subnet of N iff ex f being Function of b₃,N st
( the mapping of b₃ = the mapping of N * f & ( for m being Element of N ex n being Element of b₃ st
for p being Element of b₃ st n <= p holds
m <= f . p ) ) );