let C be category; :: thesis: ( C is terminal implies ( not C is empty & C is trivial ) )
assume A1: C is terminal ; :: thesis: ( not C is empty & C is trivial )
consider F being Functor of (OrdC 1),C such that
A2: ( F is covariant & F is bijective ) by A1, Th25, CAT_7:12;
A3: the carrier of C = rng F by A2, FUNCT_2:def 3;
A4: not C is empty by A2, CAT_6:31;
for y1, y2 being object st y1 in the carrier of C & y2 in the carrier of C holds
y1 = y2

proof

let y1, y2 be object ; :: thesis: ( y1 in the carrier of C & y2 in the carrier of C implies y1 = y2 )
assume A5: y1 in the carrier of C ; :: thesis: ( not y2 in the carrier of C or y1 = y2 )
assume A6: y2 in the carrier of C ; :: thesis: y1 = y2
consider f being morphism of (OrdC 1) such that
A7: ( f is identity & Ob (OrdC 1) = {f} & Mor (OrdC 1) = {f} ) by Th15;
reconsider x = f as object ;
dom F = the carrier of (OrdC 1) by A4, FUNCT_2:def 1;
then dom F = {f} by A7, CAT_6:def 1;
then A8: rng F = {(F . x)} by FUNCT_1:4;
hence y1 = F . x by A5, A3, TARSKI:def 1
.= y2 by A6, A8, A3, TARSKI:def 1 ;
:: thesis: verum

end;

hence ( not C is empty & C is trivial ) by A2, CAT_6:31, ZFMISC_1:def 10; :: thesis: verum