Proved Admitted lemma not_in_intersect. Had to add de-morgan axiom