let C be category; :: thesis: ( not C is empty & C is trivial implies C is terminal )
assume ( not C is empty & C is trivial ) ; :: thesis: C is terminal
then C ~= OrdC 1 by Th27;
hence C is terminal by Th26; :: thesis: verum