take id O ; :: thesis: id O is involutive
thus id O is involutive ; :: thesis: verum