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