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