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