:: deftheorem Def11 defines NetUniv YELLOW_6:def 11 :
for X being non empty 1-sorted
for b₂ being set holds
( b₂ = NetUniv X iff for x being object holds
( x in b₂ iff ex N being strict net of X st
( N = x & the carrier of N in the_universe_of the carrier of X ) ) );