take I --> {{}} ; :: thesis: I --> {{}} is total
thus I --> {{}} is total ; :: thesis: verum