consider T being non empty discrete TopSpace;
take T ; :: thesis: ( T is T_1 & not T is empty )
thus ( T is T_1 & not T is empty ) ; :: thesis: verum