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