theorem Th27: :: CAT_8:27

for C being category holds
( ( not C is empty & C is trivial ) iff C ~= OrdC 1 )