:: deftheorem Def13 defines Entr NET_1:def 13 :
for N being Pnet
for X, b₃ being set holds
( b₃ = Entr (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 = enter (N,y) ) ) ) );