let X be Subset of T; :: according to BORSUK_1:def 11 :: 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:8; :: thesis: verum