set S = the non empty non void ManySortedSign ;
take the non empty non void ManySortedSign ; :: thesis: ( not the non empty non void ManySortedSign is void & not the non empty non void ManySortedSign is empty )
thus ( not the non empty non void ManySortedSign is void & not the non empty non void ManySortedSign is empty ) ; :: thesis: verum