let X be Subset of T; :: according to BORSUK_1:def 14 :: thesis: ( not X = the carrier of (T | A) or X is closed )
thus ( not X = the carrier of (T | A) or X is closed ) by PRE_TOPC:29; :: thesis: verum