5.3ex II

All these derivations have to do with >I. But a number of other rules are involved especially =I and vE.