let C be Category; :: thesis: Alter C is transitive
let o1, o2, o3 be Object of (Alter C); :: according to ALTCAT_1:def 2 :: thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} )
assume A1: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) ; :: thesis: not <^o1,o3^> = {}
reconsider x1 = o1, x2 = o2, x3 = o3 as Object of C ;
A2: <^o1,o3^> = Hom (x1,x3) by Def3;
( <^o1,o2^> = Hom (x1,x2) & <^o2,o3^> = Hom (x2,x3) ) by Def3;
hence not <^o1,o3^> = {} by A1, A2, CAT_1:24; :: thesis: verum