take id X ; :: thesis: ( id X is total & id X is one-to-one & not id X is empty )
thus ( id X is total & id X is one-to-one & not id X is empty ) ; :: thesis: verum