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