take id X ; :: thesis: id X is onto
thus id X is onto ; :: thesis: verum