let C1, C2, C3 be composable with_identities CategoryStr ; :: thesis: ( C1 ~= C2 & C2 ~= C3 implies C1 ~= C3 )
assume A1: C1 ~= C2 ; :: thesis: ( not C2 ~= C3 or C1 ~= C3 )
assume A2: C2 ~= C3 ; :: thesis: C1 ~= C3

per cases ( ( not C2 is empty & not C3 is empty ) or C2 is empty or C3 is empty ) ;

suppose A3: ( not C2 is empty & not C3 is empty ) ; :: thesis: C1 ~= C3

consider F being Functor of C1,C2 such that
A4: ( F is covariant & F is bijective ) by A1, CAT_7:12;
consider G being Functor of C2,C3 such that
A5: ( G is covariant & G is bijective ) by A2, CAT_7:12;
F * G is onto by A4, A5, A3, FUNCT_2:27;
then G (*) F is bijective by A4, A5, CAT_6:def 27;
hence C1 ~= C3 by A4, A5, CAT_6:35, CAT_7:12; :: thesis: verum

end;

suppose ( C2 is empty or C3 is empty ) ; :: thesis: C1 ~= C3

then A6: ( C2 is empty & C3 is empty ) by A2, CAT_7:15;
then C1 is empty by A1, CAT_7:15;
hence C1 ~= C3 by A6, CAT_7:13; :: thesis: verum

end;

end;