let N be Pnet; :: thesis: for x being Element of Elements N holds
( not Elements N <> {} or exit N,x = {x} or exit N,x = Post N,x )
let x be Element of Elements N; :: thesis: ( not Elements N <> {} or exit N,x = {x} or exit N,x = Post N,x )
assume Elements N <> {} ; :: thesis: ( exit N,x = {x} or exit N,x = Post N,x )
then ( x in the Places of N or x in the Transitions of N ) by XBOOLE_0:def 3;
hence ( exit N,x = {x} or exit N,x = Post N,x ) by Def10; :: thesis: verum