let C be non empty non void CatStr ; :: thesis: ( not C is empty & C is trivial implies ( C is transitive & C is reflexive ) )
assume A1: ( not C is empty & C is trivial ) ; :: thesis: ( C is transitive & C is reflexive )
thus for f, g being Morphism of C st dom g = cod f holds
( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) by A1, ZFMISC_1:def 10; :: according to CAT_1:def 7 :: thesis: C is reflexive
let b be Element of C; :: according to CAT_1:def 9 :: thesis: Hom (b,b) <> {}
set i = the Morphism of C;
( cod the Morphism of C = b & dom the Morphism of C = b ) by A1, ZFMISC_1:def 10;
hence Hom (b,b) <> {} by Th1; :: thesis: verum