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