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