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 carrier of N or x in the carrier' of N ) by XBOOLE_0:def 3;

hence ( exit (N,x) = {x} or exit (N,x) = Post (N,x) ) by Def9; :: thesis: verum

( 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 carrier of N or x in the carrier' of N ) by XBOOLE_0:def 3;

hence ( exit (N,x) = {x} or exit (N,x) = Post (N,x) ) by Def9; :: thesis: verum