cod m = m `12 by Th13;
hence m `12 is Category by Th12; :: thesis: verum