for N being Pnet
for x being Element of Elements N st Elements N <> {} holds
exit (N,x) c= Elements N by Th19;