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