:: deftheorem Def14 defines Ext NET_1:def 14 :
for N being Pnet
for X, b₃ being set holds
( b₃ = Ext (N,X) iff for x being set holds
( x in b₃ iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = exit (N,y) ) ) ) );