for N being Pnet
for x being Element of Elements N holds
( not Elements N <> {} or exit (N,x) = {x} or exit (N,x) = Post (N,x) )