:: deftheorem Def9 defines exit NET_1:def 9 :
for N being Pnet
for x being Element of Elements N st Elements N <> {} holds
for b₃ being set holds
( b₃ = exit (N,x) iff ( ( x in the carrier of N implies b₃ = {x} ) & ( x in the carrier' of N implies b₃ = Post (N,x) ) ) );