( not [#] NTX is empty & [#] NTX is closed ) ;
hence ex b₁ being Subset of NTX st
( not b₁ is empty & b₁ is closed ) ; :: thesis: verum