take I --> 1 ; :: thesis: I --> 1 is total
thus I --> 1 is total ; :: thesis: verum