:: deftheorem defines Output NET_1:def 16 :
for N being Pnet
for X being set holds Output (N,X) = union (Ext (N,X));