[#] X = [#] (LinearTopSpaceNorm X) by NORMSP_2:def 4;
hence {} X is open by NORMSP_2:33; :: thesis: verum