take id the non empty set ; :: thesis: ( not id the non empty set is empty & id the non empty set is one-to-one )
thus ( not id the non empty set is empty & id the non empty set is one-to-one ) ; :: thesis: verum