consider S being non empty non void ManySortedSign ;
take S ; :: thesis: ( not S is void & not S is empty )
thus ( not S is void & not S is empty ) ; :: thesis: verum