[#] NTX = ([#] NTX) \ ({} NTX) ;
hence ex b₁ being Subset of NTX st b₁ is closed by Def9; :: thesis: verum