set T = the non empty discrete TopSpace;
take the non empty discrete TopSpace ; :: thesis: ( the non empty discrete TopSpace is T_1 & not the non empty discrete TopSpace is empty )
thus ( the non empty discrete TopSpace is T_1 & not the non empty discrete TopSpace is empty ) ; :: thesis: verum