take id 1 ; :: thesis: ( not id 1 is empty & id 1 is involutive )
thus ( not id 1 is empty & id 1 is involutive ) ; :: thesis: verum