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