theorem Th15: :: NET_1:15

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