thus [#] (T | X) is interval by PRE_TOPC:def 10; :: according to TOPALG_2:def 4 :: thesis: verum