( not x in the Places of N or not x in the Transitions of N ) by Th11;
hence ex b₁ being set st
( ( x in the Places of N implies b₁ = {x} ) & ( x in the Transitions of N implies b₁ = Post N,x ) ) ; :: thesis: verum