consider S being void strict ManySortedSign ;
take S ; :: thesis: ( S is strict & S is void )
thus ( S is strict & S is void ) ; :: thesis: verum