let C be category; :: thesis: ( ( not C is empty & C is trivial ) iff C ~= OrdC 1 )

hereby :: thesis: ( C ~= OrdC 1 implies ( not C is empty & C is trivial ) )

assume A1: ( not C is empty & C is trivial ) ; :: thesis: C ~= OrdC 1
consider f being morphism of (OrdC 1) such that
A2: ( f is identity & Ob (OrdC 1) = {f} & Mor (OrdC 1) = {f} ) by Th15;
ex F being Functor of C,(OrdC 1) st
( F is covariant & F is bijective )

proof

set F = the carrier of C --> f;
the carrier of (OrdC 1) = {f} by A2, CAT_6:def 1;
then f in the carrier of (OrdC 1) by TARSKI:def 1;
then reconsider F = the carrier of C --> f as Functor of C,(OrdC 1) by FUNCOP_1:45;
take F ; :: thesis: ( F is covariant & F is bijective )
for f1 being morphism of C st f1 is identity holds
F . f1 is identity

proof

let f1 be morphism of C; :: thesis: ( f1 is identity implies F . f1 is identity )
assume f1 is identity ; :: thesis: F . f1 is identity
reconsider x = f1 as object ;
not Mor C is empty by A1;
then f1 in Mor C ;
then A3: f1 in the carrier of C by CAT_6:def 1;
F . f1 = F . x by A1, CAT_6:def 21
.= f by A3, FUNCOP_1:7 ;
hence F . f1 is identity by A2; :: thesis: verum

end;

then A4: F is identity-preserving by CAT_6:def 22;
for f1, f2 being morphism of C st f1 |> f2 holds
( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) )

proof

let f1, f2 be morphism of C; :: thesis: ( f1 |> f2 implies ( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) ) )
assume f1 |> f2 ; :: thesis: ( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) )
reconsider x1 = f1, x2 = f2, x = f1 (*) f2 as object ;
not Mor C is empty by A1;
then ( f1 in Mor C & f2 in Mor C & f1 (*) f2 in Mor C ) ;
then A5: ( f1 in the carrier of C & f2 in the carrier of C & f1 (*) f2 in the carrier of C ) by CAT_6:def 1;
A6: F . f1 = F . x1 by A1, CAT_6:def 21
.= f by A5, FUNCOP_1:7 ;
A7: F . f2 = F . x2 by A1, CAT_6:def 21
.= f by A5, FUNCOP_1:7 ;
A8: F . (f1 (*) f2) = F . x by A1, CAT_6:def 21
.= f by A5, FUNCOP_1:7 ;
thus F . f1 |> F . f2 by A2, A6, A7, CAT_6:24; :: thesis: F . (f1 (*) f2) = (F . f1) (*) (F . f2)
f |> f by A2, CAT_6:24;
hence F . (f1 (*) f2) = (F . f1) (*) (F . f2) by A2, A6, A7, A8, Th4; :: thesis: verum

end;

hence F is covariant by A4, CAT_6:def 25, CAT_6:def 23; :: thesis: F is bijective
for x1, x2 being object st x1 in dom F & x2 in dom F & F . x1 = F . x2 holds
x1 = x2 by A1, ZFMISC_1:def 10;
then A9: F is one-to-one by FUNCT_1:def 4;
rng F = {f} by A1, FUNCOP_1:8
.= the carrier of (OrdC 1) by A2, CAT_6:def 1 ;
then F is onto by FUNCT_2:def 3;
hence F is bijective by A9; :: thesis: verum

end;

hence C ~= OrdC 1 by CAT_7:12; :: thesis: verum

end;

assume C ~= OrdC 1 ; :: thesis: ( not C is empty & C is trivial )
then C is terminal by Th26;
hence ( not C is empty & C is trivial ) by Lm1; :: thesis: verum