I need to wrap up Corollary 6.3.15. Moreover, I thinking of moving up 6.3.12-13-14-15 before Lemma 6.3.6