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