:: deftheorem defines Input NET_1:def 15 :
for N being Pnet
for X being set holds Input (N,X) = union (Entr (N,X));