let C, D be initial category; :: thesis: C ~= D
ex F being Functor of C,D ex G being Functor of D,C st
( F is covariant & G is covariant & G (*) F = id C & F (*) G = id D )

proof

consider F being Functor of C,D such that
A1: ( F is covariant & ( for F1 being Functor of C,D st F1 is covariant holds
F = F1 ) ) by Def8;
consider G being Functor of D,C such that
A2: ( G is covariant & ( for G1 being Functor of D,C st G1 is covariant holds
G = G1 ) ) by Def8;
take F ; :: thesis: ex G being Functor of D,C st
( F is covariant & G is covariant & G (*) F = id C & F (*) G = id D )
take G ; :: thesis: ( F is covariant & G is covariant & G (*) F = id C & F (*) G = id D )
thus ( F is covariant & G is covariant ) by A1, A2; :: thesis: ( G (*) F = id C & F (*) G = id D )
consider F1 being Functor of C,C such that
A3: ( F1 is covariant & ( for F2 being Functor of C,C st F2 is covariant holds
F1 = F2 ) ) by Def8;
thus G (*) F = F1 by A1, A2, A3, CAT_6:35
.= id C by A3 ; :: thesis: F (*) G = id D
consider G1 being Functor of D,D such that
A4: ( G1 is covariant & ( for G2 being Functor of D,D st G2 is covariant holds
G1 = G2 ) ) by Def8;
thus F (*) G = G1 by A1, A2, A4, CAT_6:35
.= id D by A4 ; :: thesis: verum

end;

hence C ~= D by CAT_6:def 28; :: thesis: verum