thus [#] (R^1 | X) is convex Subset of by PRE_TOPC:def 10; :: according to TOPALG_2:def 4 :: thesis: verum