move theorem to after a definition it depends on

(i think this theorem currently isn't used, so maybe should have just
been deleted...)