let C, D be non empty category; :: thesis: ( C is trivial & D is trivial implies C ~= D )
assume ( C is trivial & D is trivial ) ; :: thesis: C ~= D
then ( C ~= OrdC 1 & D ~= OrdC 1 ) by Th27;
hence C ~= D by Th10; :: thesis: verum