dom m = m `11 by Th13;
hence m `11 is Category by Th12; :: thesis: verum