let C1, C2 be category; :: thesis: ( C1 ~= C2 implies ( C1 is empty iff C2 is empty ) )
assume C1 ~= C2 ; :: thesis: ( C1 is empty iff C2 is empty )
then consider F being Functor of C1,C2, G being Functor of C2,C1 such that
A1: ( F is covariant & G is covariant & G (*) F = id C1 & F (*) G = id C2 ) by CAT_6:def 28;
thus ( C1 is empty iff C2 is empty ) by A1, CAT_6:31; :: thesis: verum