for N being Pnet
for x being Element of Elements N holds Post (N,x) c= Elements N