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