The extremal function for K9=minors

We prove the extremal function for K9= minors, where K9= denotes the complete graph K9 with two edges removed. In particular, we show that any graph with n >= 8 vertices and at least 6n-20 edges either contains a K9= minor or is isomorphic to a graph obtained from disjoint copies of K8 and K2,2,2,2,2 by identifying cliques of size 5. We utilize computer assistance to prove one of our lemmas.