:: deftheorem Def4 defines a_net YELLOW19:def 4 :
for L being non empty 1-sorted
for O being non empty Subset of L
for F being Filter of (BoolePoset O)
for b₄ being non empty strict NetStr over L holds
( b₄ = a_net F iff ( the carrier of b₄ = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for i, j being Element of b₄ holds
( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of b₄ holds b₄ . i = i `1 ) ) );