for N being Pnet
for x being Element of Elements N
for X being set st Elements N <> {} & x in X holds
exit (N,x) in Ext (N,X)